Janno (Jun 12 2020 at 13:29): Janno (Jun 12 2020 at 13:29):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?
Gaëtan Gilbert (Jun 12 2020 at 13:31):let p := @proj P1 .. Pn in p record_val?
Gaëtan Gilbert (Jun 12 2020 at 13:31):using ltac let
Janno (Jun 12 2020 at 13:36):That works! Thank you!
Hugo Herbelin (Sep 02 2021 at 18:58):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?
Janno (Sep 02 2021 at 21:06):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).
Janno (Sep 02 2021 at 21:08):What that means is that I am not using that hack in production. At least I hope I am not. :)
Last updated: Oct 12 2024 at 11:01 UTC