blob: 1fe91de72d5b76fe6b36a5715b791c899e6f5b9b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
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 *)
(* Now a parsing error
Fail Constraint i < Type. (* anonymous *)
*)
Set Universe Polymorphism.
Section Foo.
Universe j.
Constraint Set < j.
Definition foo := Type@{j}.
End Foo.
|
