blob: 53ef4735729df90ea8afb3816da88103fb195005 (
plain)
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
28
29
30
31
32
33
34
|
Set Universe Polymorphism.
Set Printing Universes.
Module GlobalReference.
Definition type' := Type.
Notation type := type'.
Check type@{Set}.
End GlobalReference.
Module TypeLiteral.
Notation type := Type.
Check type@{Set}.
Check type@{Prop}.
End TypeLiteral.
Module ExplicitSort.
Monomorphic Universe u.
Notation foo := Type@{u}.
Fail Check foo@{Set}.
Fail Check foo@{u}.
Notation bar := Type.
Check bar@{u}.
End ExplicitSort.
Module PropNotationUnsupported.
Notation foo := Prop.
Fail Check foo@{Set}.
Fail Check foo@{Type}.
End PropNotationUnsupported.
|
