aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/univnames.v
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'.