blob: ac5d7ea287d89df56540902521c9425b7ce90803 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
Universes i.
Fail Constraint i < Set.
Fail Constraint i <= Set.
Fail Constraint i = Set.
Constraint Set <= i.
Constraint Set < i.
Fail Constraint i < j. (* undeclared j *)
Fail Constraint i < Type. (* anonymous *)
Set Universe Polymorphism.
Section Foo.
Universe j.
Constraint Set < j.
Definition foo := Type@{j}.
End Foo.
|
