Stream: Coq devs & plugin devs

Topic: ✔ Generate a fresh constant name


view this post on Zulip Mathis Bouverot-Dupuis (Oct 01 2024 at 10:07):

Hi all, I would like to generate a fresh constant name in a given environment, using e.g. Namegen.next_global_ident_away. However I can't find how to get a Names.Id.Set.t to pass to this function.

view this post on Zulip Pierre-Marie Pédrot (Oct 01 2024 at 10:18):

with respect to what should this ident be fresh?

view this post on Zulip Pierre-Marie Pédrot (Oct 01 2024 at 10:18):

more precisely, what do you intend to do with it? add it as a hypothesis, a constant name, something else?

view this post on Zulip Mathis Bouverot-Dupuis (Oct 01 2024 at 10:18):

with respect to the global constants in the environment

view this post on Zulip Mathis Bouverot-Dupuis (Oct 01 2024 at 10:19):

I intend to add it as a constant using Declare.declare_definition

view this post on Zulip Pierre-Marie Pédrot (Oct 01 2024 at 10:19):

you can use Namegen.next_global_ident_away with an empty idset then

view this post on Zulip Mathis Bouverot-Dupuis (Oct 01 2024 at 10:20):

Oh I wasn't aware Namegen.next_global_ident_away looked into the global environment, thanks !

view this post on Zulip Notification Bot (Oct 01 2024 at 10:22):

Mathis Bouverot-Dupuis has marked this topic as resolved.


Last updated: Oct 13 2024 at 01:02 UTC