File: univnames.v

package info (click to toggle)
coq 8.20.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: sid, trixie
  • size: 44,116 kB
  • sloc: ml: 234,160; sh: 4,301; python: 3,270; ansic: 2,644; makefile: 882; lisp: 172; javascript: 63; xml: 24; sed: 2
file content (37 lines) | stat: -rw-r--r-- 934 bytes parent folder | download | duplicates (2)
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 #[export] Instance bad@{} : Wrap Type := Type.

#[export] Instance bad@{} : Wrap Type.
Fail Proof Type.
Abort.

#[export] Instance bar@{u} : Wrap@{u} Set. Proof nat.


Monomorphic Universe g.

Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'.