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.
with respect to what should this ident be fresh?
more precisely, what do you intend to do with it? add it as a hypothesis, a constant name, something else?
with respect to the global constants in the environment
I intend to add it as a constant using Declare.declare_definition
you can use Namegen.next_global_ident_away with an empty idset then
Oh I wasn't aware Namegen.next_global_ident_away
looked into the global environment, thanks !
Mathis Bouverot-Dupuis has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC