Luko van der Maas (Nov 27 2023 at 15:04): Luko van der Maas (Nov 27 2023 at 15:04):I am looking to create an elpi variant of intro ? and thus I need to create a coq free name. I can't find a way to get a free name. Is there a coq-elpi binding to free or is there some other way I should approach this?
Pierre Roux (Nov 27 2023 at 16:08):What about https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi#L810-L814
Luko van der Maas (Nov 27 2023 at 16:16):That only takes into account the global environment, so if I already have an a in the context of my goal and then I use
coq.env.fresh-global-id "a" ID
ID still becomes ¨a"
Enrico Tassi (Nov 27 2023 at 16:29):Coq's Namegen module has an API for that, but one needs to bind it. Could you please open an issue?
Luko van der Maas (Nov 27 2023 at 16:30):I will do so now
Luko van der Maas (Nov 27 2023 at 16:32):https://github.com/LPCIC/coq-elpi/issues/554
Last updated: Oct 13 2024 at 01:02 UTC