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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
|
Inductive Empty@{uu} : Type@{uu} := .
(* uu |= *)
Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap
{ punwrap : A }.
(* uu |= *)
PWrap has primitive projections with eta conversion.
Arguments PWrap _%type_scope
Arguments pwrap _%type_scope _
punwrap@{uu} =
fun (A : Type@{uu}) (p : PWrap@{uu} A) => punwrap _ p
: forall A : Type@{uu}, PWrap@{uu} A -> A
(* uu |= *)
Arguments punwrap _%type_scope _
Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap
{ runwrap : A }.
(* uu |= *)
Arguments RWrap _%type_scope
Arguments rwrap _%type_scope _
runwrap@{uu} =
fun (A : Type@{uu}) (r : RWrap@{uu} A) => let (runwrap) := r in runwrap
: forall A : Type@{uu}, RWrap@{uu} A -> A
(* uu |= *)
Arguments runwrap _%type_scope _
Wrap@{uu} = fun A : Type@{uu} => A
: Type@{uu} -> Type@{uu}
(* uu |= *)
Arguments Wrap _%type_scope
wrap@{uu} =
fun (A : Type@{uu}) (Wrap : Wrap@{uu} A) => Wrap
: forall A : Type@{uu}, Wrap@{uu} A -> A
(* uu |= *)
Arguments wrap {A}%type_scope {Wrap}
bar@{uu} = nat
: Wrap@{uu} Set
(* uu |= Set < uu *)
foo@{uu u v} =
Type@{u} -> Type@{v} -> Type@{uu}
: Type@{max(uu+1,u+1,v+1)}
(* uu u v |= *)
Type@{i} -> Type@{j}
: Type@{max(i+1,j+1)}
(* {j i} |= *)
= Type@{i} -> Type@{j}
: Type@{max(i+1,j+1)}
(* {j i} |= *)
mono = Type@{mono.uu}
: Type@{mono.uu+1}
(* {mono.uu} |= *)
mono
: Type@{mono.uu+1}
Type@{mono.uu}
: Type@{mono.uu+1}
The command has indeed failed with message:
Universe uu already exists.
monomono
: Type@{MONOU+1}
mono.monomono
: Type@{mono.MONOU+1}
monomono
: Type@{MONOU+1}
mono
: Type@{mono.uu+1}
The command has indeed failed with message:
Universe uu already exists.
bobmorane =
let tt := Type@{UnivBinders.32} in
let ff := Type@{UnivBinders.34} in tt -> ff
: Type@{max(UnivBinders.31,UnivBinders.33)}
The command has indeed failed with message:
Universe uu already bound.
foo@{E M N} =
Type@{M} -> Type@{N} -> Type@{E}
: Type@{max(E+1,M+1,N+1)}
(* E M N |= *)
foo@{uu u v} =
Type@{u} -> Type@{v} -> Type@{uu}
: Type@{max(uu+1,u+1,v+1)}
(* uu u v |= *)
Inductive Empty@{E} : Type@{E} := .
(* E |= *)
Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }.
(* E |= *)
PWrap has primitive projections with eta conversion.
Arguments PWrap _%type_scope
Arguments pwrap _%type_scope _
punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A
(* K |= *)
punwrap is universe polymorphic
Arguments punwrap _%type_scope _
punwrap is transparent
Expands to: Constant UnivBinders.punwrap
The command has indeed failed with message:
Universe instance should have length 3
The command has indeed failed with message:
Universe instance should have length 0
The command has indeed failed with message:
This object does not support universe names.
The command has indeed failed with message:
Cannot enforce v < u because u < gU < gV < v
insec@{v} = Type@{uu} -> Type@{v}
: Type@{max(uu+1,v+1)}
(* v |= *)
Inductive insecind@{k} : Type@{k+1} :=
inseccstr : Type@{k} -> insecind@{k}.
(* k |= *)
Arguments inseccstr _%type_scope
insec@{uu v} = Type@{uu} -> Type@{v}
: Type@{max(uu+1,v+1)}
(* uu v |= *)
Inductive insecind@{uu k} : Type@{k+1} :=
inseccstr : Type@{k} -> insecind@{uu k}.
(* uu k |= *)
Arguments inseccstr _%type_scope
insec2@{u} = Prop
: Type@{Set+1}
(* u |= *)
inmod@{uu} = Type@{uu}
: Type@{uu+1}
(* uu |= *)
SomeMod.inmod@{uu} = Type@{uu}
: Type@{uu+1}
(* uu |= *)
inmod@{uu} = Type@{uu}
: Type@{uu+1}
(* uu |= *)
Applied.infunct@{uu v} =
inmod@{uu} -> Type@{v}
: Type@{max(uu+1,v+1)}
(* uu v |= *)
axfoo@{i u u0} : Type@{u} -> Type@{i}
(* i u u0 |= *)
axfoo is universe polymorphic
Arguments axfoo _%type_scope
Expands to: Constant UnivBinders.axfoo
axbar@{i u u0} : Type@{u0} -> Type@{i}
(* i u u0 |= *)
axbar is universe polymorphic
Arguments axbar _%type_scope
Expands to: Constant UnivBinders.axbar
axfoo' : Type@{axfoo'.u0} -> Type@{axfoo'.i}
axfoo' is not universe polymorphic
Arguments axfoo' _%type_scope
Expands to: Constant UnivBinders.axfoo'
axbar' : Type@{axfoo'.u0} -> Type@{axfoo'.i}
axbar' is not universe polymorphic
Arguments axbar' _%type_scope
Expands to: Constant UnivBinders.axbar'
The command has indeed failed with message:
When declaring multiple axioms in one command, only the first is allowed a universe binder (which will be shared by the whole block).
foo@{i} = Type@{M.i} -> Type@{i}
: Type@{max(M.i+1,i+1)}
(* i |= *)
Type@{u0} -> Type@{UnivBinders.64}
: Type@{max(u0+1,UnivBinders.64+1)}
(* {UnivBinders.64} |= *)
bind_univs.mono =
Type@{bind_univs.mono.u}
: Type@{bind_univs.mono.u+1}
(* {bind_univs.mono.u} |= *)
bind_univs.poly@{u} = Type@{u}
: Type@{u+1}
(* u |= *)
|
