Enrico Tassi (Jun 13 2022 at 14:33): Enrico Tassi (Jun 13 2022 at 14:33):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...
Enrico Tassi (Jun 13 2022 at 14:34):Apparently only named universes can be used as universe binders in a universe polymorphic declaration
Enrico Tassi (Jun 13 2022 at 14:34):CC @Gaëtan Gilbert @Pierre-Marie Pédrot
Gaëtan Gilbert (Jun 13 2022 at 14:34):Enrico Tassi said:
Apparently only named universes can be used as universe binders in a universe polymorphic declaration
how else would it work?
Gaëtan Gilbert (Jun 13 2022 at 14:34):wdym by "used as universe binders" exactly?
Gaëtan Gilbert (Jun 13 2022 at 14:37):what does the api look like now and what do you want to change?
Enrico Tassi (Jun 13 2022 at 14:39):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).
Enrico Tassi (Jun 13 2022 at 14:39):Evd.new_univ_level_variable takes an optional name, so some levels don't have one
Enrico Tassi (Jun 13 2022 at 14:40):I can' systematically give them a name u1 ... un so that the user does not need to name them explicitly...
Gaëtan Gilbert (Jun 13 2022 at 14:45):we can probably change UState.universe_decl so it contains a level list instead of names
Gaëtan Gilbert (Jun 13 2022 at 14:53):https://github.com/coq/coq/pull/16180
Enrico Tassi (Jun 14 2022 at 08:02):Thanks for the PR!
Paolo Giarrusso (Jun 14 2022 at 09:15):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
Gaëtan Gilbert (Jun 14 2022 at 09:23):names of polymorphic univs are irrelevant for that
Last updated: May 28 2023 at 13:30 UTC