blob: 86597c88faa07403f7cb9d04ff47fbf117ca3ba4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
Section foo.
Polymorphic Universes A B.
Fail Constraint A <= B.
End foo.
(* gives an anomaly Universe undefined *)
Universes X Y.
Section Foo.
Polymorphic Universes Z W.
Polymorphic Constraint W < Z.
Fail Definition bla := Type@{W}.
Polymorphic Definition bla := Type@{W}.
Section Bar.
Fail Constraint X <= Z.
End Bar.
End Foo.
|
