Does it have a cost to give a name (even a generated one) to all universes?
In the context of Elpi I'm trying to simplify an API...
Apparently only named universes can be used as universe binders in a universe polymorphic declaration
CC @Gaëtan Gilbert @Pierre-Marie Pédrot
Enrico Tassi said:
Apparently only named universes can be used as universe binders in a universe polymorphic declaration
how else would it work?
wdym by "used as universe binders" exactly?
what does the api look like now and what do you want to change?
Declare.Info.make
takes a UState.gen_universe_decl
where the binders are names, while I'm giving the user an API where I used the levels directly (since he can named them using the variables of the programming language, rather than strings).
Evd.new_univ_level_variable
takes an optional name, so some levels don't have one
I can' systematically give them a name u1
... un
so that the user does not need to name them explicitly...
we can probably change UState.universe_decl so it contains a level list instead of names
https://github.com/coq/coq/pull/16180
Thanks for the PR!
Re the option where “all universes have a name”, would those names be usable in Coq, right? That’d help with commands that demand users to name a universe, like https://coq.inria.fr/refman/addendum/universe-polymorphism.html#coq:cmd.Print-Universes
names of polymorphic univs are irrelevant for that
Last updated: Nov 29 2023 at 05:01 UTC