blob: 666c64631f707e122b73af5ab2ab4657084b92d9 (
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
|
Set Universe Polymorphism.
Set Printing Universes.
Axiom foo@{i j} : Type@{i} -> Type@{j}.
Notation bar := foo.
Monomorphic Universes i j.
Check bar@{i j}.
Fail Check bar@{i}.
Notation qux := (nat -> nat).
Fail Check qux@{i}.
Axiom TruncType@{i} : nat -> Type@{i}.
Notation "n -Type" := (TruncType n) (at level 1) : type_scope.
Notation hProp := (0)-Type.
Check hProp.
Check hProp@{i}.
|
