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: Sep 23 2023 at 13:01 UTC