Gregory Malecha (Feb 11 2022 at 14:25): 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?
Gaëtan Gilbert (Feb 11 2022 at 14:27):works for me
Gregory Malecha (Feb 11 2022 at 14:30):Ooops, I got my example wrong. Thanks
Notification Bot (Feb 14 2022 at 14:09):Ali Caglayan has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC