Stream: Coq users

Topic: Match on "match-with" hypothesis, regardless of type


view this post on Zulip spaceloop (Mar 30 2022 at 09:30):

Is it possible in ltac to match on a hypothesis of the form match ?z with _ end, regardless of the type being matched (i.e. without specifying the branches).

view this post on Zulip Janno (Mar 30 2022 at 09:32):

Yes. The magic incantation is match ?z with _ => _ end.

view this post on Zulip spaceloop (Mar 30 2022 at 09:35):

Thanks!


Last updated: Mar 28 2024 at 20:01 UTC