Stream: Coq devs & plugin devs

Topic: ✔ Explicitly declared universes can not be qualified


view this post on Zulip Gregory Malecha (Feb 11 2022 at 14:25):

I just wrote the following and found it odd.

(* foo.v *)
Universe BIG.
(* bar.v *)
Require Import foo.
Fail Definition t : Type@{foo.BIG}.
Definition t : Type@{BIG} := nat.

Is there a reason why universe names are not scoped the way that other names are? How would I distinguish between two universes declared in different files but have the same name?

view this post on Zulip Gaëtan Gilbert (Feb 11 2022 at 14:27):

works for me

view this post on Zulip Gregory Malecha (Feb 11 2022 at 14:30):

Ooops, I got my example wrong. Thanks

view this post on Zulip Notification Bot (Feb 14 2022 at 14:09):

Ali Caglayan has marked this topic as resolved.


Last updated: Feb 06 2023 at 18:03 UTC