blob: 048b53d26c85a739f4088e602861ff794a17e8e1 (
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
|
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.
Monomorphic Universe g.
Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'.
|
