Stream: Coq users

Topic: Ltac2 & Primitive Projections

Janno (Sep 04 2020 at 15:12):

Is there a nice way to match! on projections in Ltac2 such that the branch also matches the primitive, unfolded form of the projection?

Last updated: Jan 29 2023 at 05:03 UTC