1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
Module Pt1.
Module M. Universe i. End M.
Module N. Universe i. End N.
Import M.
Notation foo := Type@{i (* M.i??? *)}.
Import N.
Fail Check foo : Type@{M.i}. (* should NOT succeed *)
Check foo : Type@{i (* N.i *)}. (* should succeed *)
Definition bar@{i} := Type@{i}.
Check bar : Type@{N.i}.
Check bar : Type@{M.i}.
End Pt1.
Module Pt2.
Module M. Universe i. Notation foo := Type@{i}. End M.
Definition foo1 := M.foo.
(* should succeed, currently errors undeclared universe i *)
Definition foo2@{i} : Type@{i} := M.foo.
(* should succeed, currently errors universe inconsistency *)
End Pt2.
|
