blob: fe3b8c1d7c3b62e0de8bda33eab57afa119ae48f (
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
35
36
37
|
Set Universe Polymorphism.
Definition foo@{i j} (A : Type@{i}) (B : Type@{j}) := A.
Set Printing Universes.
Fail Definition bar@{i} (A : Type@{i}) (B : Type) := A.
Definition baz@{i j} (A : Type@{i}) (B : Type@{j}) := (A * B)%type.
Fail Definition bad@{i j} (A : Type@{i}) (B : Type@{j}) : Type := (A * B)%type.
Fail Definition bad@{i} (A : Type@{i}) (B : Type@{j}) : Type := (A * B)%type.
Definition shuffle@{i j} (A : Type@{j}) (B : Type@{i}) := (A * B)%type.
Definition nothing (A : Type) := A.
Inductive bla@{l k} : Type@{k} := blaI : Type@{l} -> bla.
Inductive blacopy@{k l} : Type@{k} := blacopyI : Type@{l} -> blacopy.
Class Wrap A := wrap : A.
Fail Instance bad@{} : Wrap Type := Type.
Instance bad@{} : Wrap Type.
Fail Proof Type.
Abort.
Instance bar@{u} : Wrap@{u} Set. Proof nat.
Monomorphic Universe g.
Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'.
|
