Is there a nice way to match! on projections in Ltac2 such that the branch also matches the primitive, unfolded form of the projection?
match!
Last updated: Apr 16 2024 at 10:01 UTC
Janno (Sep 04 2020 at 15:12): Janno (Sep 04 2020 at 15:12):