Stream: Coq devs & plugin devs

Topic: Named v.s. Unnamed universe levels


view this post on Zulip 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...

view this post on Zulip Enrico Tassi (Jun 13 2022 at 14:34):

Apparently only named universes can be used as universe binders in a universe polymorphic declaration

view this post on Zulip Enrico Tassi (Jun 13 2022 at 14:34):

CC @Gaëtan Gilbert @Pierre-Marie Pédrot

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Jun 13 2022 at 14:34):

wdym by "used as universe binders" exactly?

view this post on Zulip Gaëtan Gilbert (Jun 13 2022 at 14:37):

what does the api look like now and what do you want to change?

view this post on Zulip 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).

view this post on Zulip Enrico Tassi (Jun 13 2022 at 14:39):

Evd.new_univ_level_variable takes an optional name, so some levels don't have one

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Jun 13 2022 at 14:53):

https://github.com/coq/coq/pull/16180

view this post on Zulip Enrico Tassi (Jun 14 2022 at 08:02):

Thanks for the PR!

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Jun 14 2022 at 09:23):

names of polymorphic univs are irrelevant for that


Last updated: Nov 29 2023 at 05:01 UTC