Stream: Coq devs & plugin devs

Topic: Primitive Projections


view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Jun 12 2020 at 13:31):

let p := @proj P1 .. Pn in p record_val?

view this post on Zulip Gaëtan Gilbert (Jun 12 2020 at 13:31):

using ltac let

view this post on Zulip Janno (Jun 12 2020 at 13:36):

That works! Thank you!

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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 16 2021 at 09:07 UTC