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: Oct 13 2024 at 01:02 UTC
Janno (Sep 04 2020 at 15:12): Janno (Sep 04 2020 at 15:12):