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).
Yes. The magic incantation is match ?z with _ => _ end
.
Thanks!
Last updated: Mar 28 2024 at 20:01 UTC