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
|
NonCumulative Inductive Empty@{u} : Type@{u} :=
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 _]
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 _]
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 _]
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 _]
Wrap@{u} = fun A : Type@{u} => A
: Type@{u} -> Type@{u}
(* u |= *)
Wrap is universe polymorphic
Argument scope is [type_scope]
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 _]
bar@{u} = nat
: Wrap@{u} Set
(* u |= Set < u
*)
bar is universe polymorphic
foo@{u Top.17 v} =
Type@{Top.17} -> Type@{v} -> Type@{u}
: Type@{max(u+1,Top.17+1,v+1)}
(* u Top.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.
bobmorane =
let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff
: Type@{max(tt.u,ff.u)}
The command has indeed failed with message:
Universe u already bound.
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
foo@{Top.16 Top.17 Top.18} =
Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16}
: Type@{max(Top.16+1,Top.17+1,Top.18+1)}
(* Top.16 Top.17 Top.18 |= *)
foo is universe polymorphic
NonCumulative Inductive Empty@{E} : Type@{E} :=
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 Top.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
bind_univs.poly@{u} = Type@{u}
: Type@{u+1}
(* u |= *)
bind_univs.poly is universe polymorphic
insec@{v} = Type@{u} -> Type@{v}
: Type@{max(u+1,v+1)}
(* v |= *)
insec is universe polymorphic
insec@{u v} = Type@{u} -> Type@{v}
: Type@{max(u+1,v+1)}
(* u v |= *)
insec is universe polymorphic
inmod@{u} = Type@{u}
: Type@{u+1}
(* u |= *)
inmod is universe polymorphic
SomeMod.inmod@{u} = Type@{u}
: Type@{u+1}
(* u |= *)
SomeMod.inmod is universe polymorphic
inmod@{u} = Type@{u}
: Type@{u+1}
(* u |= *)
inmod is universe polymorphic
Applied.infunct@{u v} =
inmod@{u} -> Type@{v}
: Type@{max(u+1,v+1)}
(* u v |= *)
Applied.infunct is universe polymorphic
axfoo@{i Top.48 Top.49} : Type@{Top.48} -> Type@{i}
(* i Top.48 Top.49 |= *)
axfoo is universe polymorphic
Argument scope is [type_scope]
Expands to: Constant Top.axfoo
axbar@{i Top.48 Top.49} : Type@{Top.49} -> Type@{i}
(* i Top.48 Top.49 |= *)
axbar is universe polymorphic
Argument scope is [type_scope]
Expands to: Constant Top.axbar
axfoo' : Type@{Top.51} -> Type@{axbar'.i}
axfoo' is not universe polymorphic
Argument scope is [type_scope]
Expands to: Constant Top.axfoo'
axbar' : Type@{Top.51} -> Type@{axbar'.i}
axbar' is not universe polymorphic
Argument scope is [type_scope]
Expands to: Constant Top.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).
|
