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
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
|
Polymorphic NonCumulative Inductive Empty@{u} : Type@{u} :=
Polymorphic NonCumulative Record PWrap (A : Type@{u}) : Type@{u} := pwrap
{ punwrap : A }
PWrap has primitive projections with eta conversion.
For PWrap: Argument scope is [type_scope]
For pwrap: Argument scopes are [type_scope _]
Polymorphic punwrap@{u} =
fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p
: forall A : Type@{u}, PWrap@{u} A -> A
(* u |= *)
punwrap is universe polymorphic
Argument scopes are [type_scope _]
Polymorphic NonCumulative Record RWrap (A : Type@{u}) : Type@{u} := rwrap
{ runwrap : A }
For RWrap: Argument scope is [type_scope]
For rwrap: Argument scopes are [type_scope _]
Polymorphic runwrap@{u} =
fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap
: forall A : Type@{u}, RWrap@{u} A -> A
(* u |= *)
runwrap is universe polymorphic
Argument scopes are [type_scope _]
Polymorphic Wrap@{u} =
fun A : Type@{u} => A
: Type@{u} -> Type@{u}
(* u |= *)
Wrap is universe polymorphic
Argument scope is [type_scope]
Polymorphic wrap@{u} =
fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap
: forall A : Type@{u}, Wrap@{u} A -> A
(* u |= *)
wrap is universe polymorphic
Arguments A, Wrap are implicit and maximally inserted
Argument scopes are [type_scope _]
Polymorphic bar@{u} = nat
: Wrap@{u} Set
(* u |= Set < u
*)
bar is universe polymorphic
Polymorphic foo@{u UnivBinders.17 v} =
Type@{UnivBinders.17} -> Type@{v} -> Type@{u}
: Type@{max(u+1,UnivBinders.17+1,v+1)}
(* u UnivBinders.17 v |= *)
foo is universe polymorphic
Type@{i} -> Type@{j}
: Type@{max(i+1,j+1)}
(* {j i} |= *)
= Type@{i} -> Type@{j}
: Type@{max(i+1,j+1)}
(* {j i} |= *)
Monomorphic mono = Type@{mono.u}
: Type@{mono.u+1}
(* {mono.u} |= *)
mono is not universe polymorphic
mono
: Type@{mono.u+1}
Type@{mono.u}
: Type@{mono.u+1}
The command has indeed failed with message:
Universe u already exists.
monomono
: Type@{MONOU+1}
mono.monomono
: Type@{mono.MONOU+1}
monomono
: Type@{MONOU+1}
mono
: Type@{mono.u+1}
The command has indeed failed with message:
Universe u already exists.
Monomorphic bobmorane =
let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff
: Type@{max(tt.u,ff.u)}
bobmorane is not universe polymorphic
The command has indeed failed with message:
Universe u already bound.
Polymorphic foo@{E M N} =
Type@{M} -> Type@{N} -> Type@{E}
: Type@{max(E+1,M+1,N+1)}
(* E M N |= *)
foo is universe polymorphic
Polymorphic foo@{u UnivBinders.17 v} =
Type@{UnivBinders.17} -> Type@{v} -> Type@{u}
: Type@{max(u+1,UnivBinders.17+1,v+1)}
(* u UnivBinders.17 v |= *)
foo is universe polymorphic
Polymorphic NonCumulative Inductive Empty@{E} : Type@{E} :=
Polymorphic NonCumulative Record PWrap (A : Type@{E}) : Type@{E} := pwrap
{ punwrap : A }
PWrap has primitive projections with eta conversion.
For PWrap: Argument scope is [type_scope]
For pwrap: Argument scopes are [type_scope _]
punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A
(* K |= *)
punwrap is universe polymorphic
Argument scopes are [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
Monomorphic bind_univs.mono =
Type@{bind_univs.mono.u}
: Type@{bind_univs.mono.u+1}
(* {bind_univs.mono.u} |= *)
bind_univs.mono is not universe polymorphic
Polymorphic bind_univs.poly@{u} = Type@{u}
: Type@{u+1}
(* u |= *)
bind_univs.poly is universe polymorphic
Polymorphic insec@{v} =
Type@{u} -> Type@{v}
: Type@{max(u+1,v+1)}
(* v |= *)
insec is universe polymorphic
Polymorphic NonCumulative Inductive insecind@{k} : Type@{k+1} :=
inseccstr : Type@{k} -> insecind@{k}
For inseccstr: Argument scope is [type_scope]
Polymorphic insec@{u v} =
Type@{u} -> Type@{v}
: Type@{max(u+1,v+1)}
(* u v |= *)
insec is universe polymorphic
Polymorphic NonCumulative Inductive insecind@{u k} : Type@{k+1} :=
inseccstr : Type@{k} -> insecind@{u k}
For inseccstr: Argument scope is [type_scope]
Polymorphic insec2@{u} = Prop
: Type@{Set+1}
(* u |= *)
insec2 is universe polymorphic
Polymorphic inmod@{u} = Type@{u}
: Type@{u+1}
(* u |= *)
inmod is universe polymorphic
Polymorphic SomeMod.inmod@{u} = Type@{u}
: Type@{u+1}
(* u |= *)
SomeMod.inmod is universe polymorphic
Polymorphic inmod@{u} = Type@{u}
: Type@{u+1}
(* u |= *)
inmod is universe polymorphic
Polymorphic Applied.infunct@{u v} =
inmod@{u} -> Type@{v}
: Type@{max(u+1,v+1)}
(* u v |= *)
Applied.infunct is universe polymorphic
axfoo@{i UnivBinders.56 UnivBinders.57} :
Type@{UnivBinders.56} -> Type@{i}
(* i UnivBinders.56 UnivBinders.57 |= *)
axfoo is universe polymorphic
Argument scope is [type_scope]
Expands to: Constant UnivBinders.axfoo
axbar@{i UnivBinders.56 UnivBinders.57} :
Type@{UnivBinders.57} -> Type@{i}
(* i UnivBinders.56 UnivBinders.57 |= *)
axbar is universe polymorphic
Argument scope is [type_scope]
Expands to: Constant UnivBinders.axbar
axfoo' : Type@{UnivBinders.59} -> Type@{axbar'.i}
axfoo' is not universe polymorphic
Argument scope is [type_scope]
Expands to: Constant UnivBinders.axfoo'
axbar' : Type@{UnivBinders.59} -> Type@{axbar'.i}
axbar' is not universe polymorphic
Argument scope is [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).
|
