Is there a way to enter
@proj P1 .. Pn record_val for
record_val of a primitive record type with parameters
P1 .. Pn without it automatically being unfolded to the primitive projection?
let p := @proj P1 .. Pn in p record_val?
using ltac let
That works! Thank you!
Hi @Janno, I see this message late and I have a question in passing. If all enough-applied projections in "primitive" records were systematically represented in a compact way, which would probably break the
let-based "trick" above, what would you lose? (I'm asking because this is one of the options mentioned in this discussion on primitive projections.)
Alternatively, if you'd lose something, would defining your own non-compactly-represented
Definition proj' P1 ... Pn record_eval := @proj P1 .. Pn record_val be enough to suit your needs?
I think I needed this trick only for debugging issues with primitive projections in Mtac2 and unicoq. Though I can't quite remember the context of my question. Judging by the date it was probably related to this issue here https://github.com/unicoq/unicoq/issues/44 (long fixed).
What that means is that I am not using that hack in production. At least I hope I am not. :)
Last updated: Oct 16 2021 at 09:07 UTC