-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathUnstar.glob
390 lines (390 loc) · 16.2 KB
/
Unstar.glob
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
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
DIGEST b9063f310b52954f86f4dbc019ab7b50
FUnstar
R1992:1996 Coq.Arith.Arith <> <> lib
R2014:2017 Coq.Lists.List <> <> lib
R2035:2037 Coq.Arith.Max <> <> lib
R2056:2059 Test <> <> lib
R2077:2083 General <> <> lib
R2102:2112 LamSF_Terms <> <> lib
R2130:2152 LamSF_Substitution_term <> <> lib
R2170:2182 LamSF_Tactics <> <> lib
R2200:2209 Components <> <> lib
R2227:2235 Compounds <> <> lib
R2253:2267 LamSF_reduction <> <> lib
R2285:2296 LamSF_Normal <> <> lib
R2314:2325 LamSF_Closed <> <> lib
R2343:2352 LamSF_Eval <> <> lib
R2370:2384 type_derivation <> <> lib
R2402:2421 type_derivation_resi <> <> lib
R2439:2452 operator_types <> <> lib
R2471:2487 subject_reduction <> <> lib
R2506:2510 Equal <> <> lib
def 2526:2532 <> id_type
R2537:2539 LamSF_Terms <> Abs constr
R2542:2546 type_derivation <> funty def
R2557:2559 LamSF_Terms <> Ref constr
R2549:2551 LamSF_Terms <> Ref constr
def 2579:2581 <> ref
R2586:2588 LamSF_Terms <> Ref constr
def 2603:2604 <> ap
R2609:2611 LamSF_Terms <> App constr
def 2627:2629 <> abs
R2634:2636 LamSF_Terms <> Abs constr
def 2651:2655 <> abs_S
R2661:2663 Unstar <> abs def
R2666:2668 Unstar <> abs def
R2671:2673 Unstar <> abs def
R2676:2677 Unstar <> ap def
R2701:2702 Unstar <> ap def
R2713:2715 Unstar <> ref def
R2705:2707 Unstar <> ref def
R2680:2681 Unstar <> ap def
R2692:2694 Unstar <> ref def
R2684:2686 Unstar <> ref def
def 2739:2743 <> abs_K
R2749:2751 Unstar <> abs def
R2754:2756 Unstar <> abs def
R2759:2761 Unstar <> ref def
def 2780:2784 <> abs_I
R2790:2792 Unstar <> abs def
R2795:2797 Unstar <> ref def
def 2815:2820 <> abs_KI
R2826:2828 Unstar <> abs def
R2831:2833 Unstar <> abs def
R2836:2838 Unstar <> ref def
prf 2855:2864 <> abs_S_type
R2868:2877 type_derivation <> derivation ind
R2890:2893 type_derivation <> opty def
R2895:2897 LamSF_Terms <> Sop constr
R2883:2887 Unstar <> abs_S def
R2879:2881 Coq.Init.Datatypes <> nil constr
R2916:2920 Unstar <> abs_S def
R2943:2945 Unstar <> abs def
R2948:2949 Unstar <> ap def
R2967:2977 type_derivation <> derive_gen1 constr
R2967:2977 type_derivation <> derive_gen1 constr
R2967:2977 type_derivation <> derive_gen1 constr
R2967:2977 type_derivation <> derive_gen1 constr
R2967:2977 type_derivation <> derive_gen1 constr
R3003:3012 type_derivation <> derive_abs constr
R3003:3012 type_derivation <> derive_abs constr
R3003:3012 type_derivation <> derive_abs constr
R3003:3012 type_derivation <> derive_abs constr
R3003:3012 type_derivation <> derive_abs constr
R3030:3039 type_derivation <> derive_app constr
R3030:3039 type_derivation <> derive_app constr
R3030:3039 type_derivation <> derive_app constr
R3030:3039 type_derivation <> derive_app constr
R3030:3039 type_derivation <> derive_app constr
R3030:3039 type_derivation <> derive_app constr
R3030:3039 type_derivation <> derive_app constr
R3030:3039 type_derivation <> derive_app constr
prf 3065:3074 <> abs_K_type
R3078:3087 type_derivation <> derivation ind
R3100:3103 type_derivation <> opty def
R3105:3107 LamSF_Terms <> Kop constr
R3093:3097 Unstar <> abs_K def
R3089:3091 Coq.Init.Datatypes <> nil constr
R3126:3130 Unstar <> abs_K def
R3153:3155 Unstar <> abs def
R3158:3159 Unstar <> ap def
R3177:3187 type_derivation <> derive_gen1 constr
R3177:3187 type_derivation <> derive_gen1 constr
R3177:3187 type_derivation <> derive_gen1 constr
R3177:3187 type_derivation <> derive_gen1 constr
R3213:3222 type_derivation <> derive_abs constr
R3213:3222 type_derivation <> derive_abs constr
R3213:3222 type_derivation <> derive_abs constr
R3213:3222 type_derivation <> derive_abs constr
R3240:3249 type_derivation <> derive_app constr
R3240:3249 type_derivation <> derive_app constr
def 3284:3288 <> abs_A
R3295:3297 LamSF_Terms <> Abs constr
R3300:3302 LamSF_Terms <> Abs constr
R3305:3307 LamSF_Terms <> App constr
R3312:3314 LamSF_Terms <> App constr
R3325:3327 LamSF_Terms <> Ref constr
R3317:3319 LamSF_Terms <> Ref constr
R3309:3309 Unstar <> u var
prf 3343:3352 <> abs_A_type
R3356:3365 type_derivation <> derivation ind
R3403:3406 type_derivation <> opty def
R3408:3410 LamSF_Terms <> Aop constr
R3387:3391 Unstar <> abs_A def
R3394:3396 LamSF_Terms <> Ref constr
R3368:3371 Coq.Init.Datatypes <> cons constr
R3381:3383 Coq.Init.Datatypes <> nil constr
R3373:3379 Unstar <> id_type def
R3430:3434 Unstar <> abs_A def
R3465:3475 type_derivation <> derive_gen1 constr
R3465:3475 type_derivation <> derive_gen1 constr
R3465:3475 type_derivation <> derive_gen1 constr
R3465:3475 type_derivation <> derive_gen1 constr
R3486:3489 LamSF_Terms <> lift def
R3514:3528 LamSF_Closed <> lift_rec_closed thm
R3514:3528 LamSF_Closed <> lift_rec_closed thm
R3563:3570 LamSF_Terms <> relocate def
R3595:3604 type_derivation <> derive_abs constr
R3595:3604 type_derivation <> derive_abs constr
R3595:3604 type_derivation <> derive_abs constr
R3595:3604 type_derivation <> derive_abs constr
R3622:3631 type_derivation <> derive_app constr
R3622:3631 type_derivation <> derive_app constr
R3622:3631 type_derivation <> derive_app constr
R3622:3631 type_derivation <> derive_app constr
R3622:3631 type_derivation <> derive_app constr
R3622:3631 type_derivation <> derive_app constr
R3642:3656 type_derivation <> derive_instance thm
R3642:3656 type_derivation <> derive_instance thm
R3680:3687 LamSF_Tactics <> succ_red constr
R3680:3687 LamSF_Tactics <> succ_red constr
R3697:3709 type_derivation <> instance_rule constr
R3697:3709 type_derivation <> instance_rule constr
R3742:3746 type_derivation <> varty def
R3771:3775 LamSF_Terms <> subst def
R3817:3829 LamSF_Substitution_term <> lift_rec_null thm
R3817:3829 LamSF_Substitution_term <> lift_rec_null thm
R3817:3829 LamSF_Substitution_term <> lift_rec_null thm
R3840:3847 LamSF_Tactics <> zero_red constr
def 3909:3917 <> unstar_fn
R3923:3925 LamSF_Terms <> Abs constr
R3928:3930 LamSF_Terms <> App constr
R3939:3941 LamSF_Terms <> App constr
R3976:3978 LamSF_Terms <> App constr
R4004:4006 LamSF_Terms <> App constr
R4014:4016 LamSF_Terms <> App constr
R4040:4043 Components <> i_op def
R4019:4021 LamSF_Terms <> App constr
R4033:4037 Unstar <> abs_S def
R4024:4025 LamSF_Terms <> Op constr
R4027:4030 LamSF_Terms <> DSop constr
R4008:4011 Components <> g_op def
R3981:3983 LamSF_Terms <> App constr
R3995:3999 Unstar <> abs_K def
R3986:3987 LamSF_Terms <> Op constr
R3989:3992 LamSF_Terms <> DKop constr
R3944:3946 LamSF_Terms <> App constr
R3959:3963 Unstar <> abs_A def
R3966:3968 LamSF_Terms <> Ref constr
R3949:3950 LamSF_Terms <> Op constr
R3952:3955 LamSF_Terms <> DAop constr
R3932:3935 Components <> g_op def
def 4064:4069 <> unstar
R4074:4076 LamSF_Terms <> App constr
R4094:4102 Unstar <> unstar_fn def
R4079:4081 LamSF_Terms <> App constr
R4088:4091 Components <> y_op def
R4083:4086 Components <> a_op def
prf 4752:4762 <> unstar_type
R4765:4774 type_derivation <> derivation ind
R4788:4790 LamSF_Terms <> Abs constr
R4793:4797 type_derivation <> funty def
R4810:4814 type_derivation <> varty def
R4800:4804 type_derivation <> varty def
R4780:4785 Unstar <> unstar def
R4776:4778 Coq.Init.Datatypes <> nil constr
R4837:4842 Unstar <> unstar def
R4853:4862 type_derivation <> derive_app constr
R4853:4862 type_derivation <> derive_app constr
R4873:4882 type_derivation <> derive_app constr
R4873:4882 type_derivation <> derive_app constr
R4893:4900 operator_types <> derive_A thm
R4893:4900 operator_types <> derive_A thm
R4939:4946 operator_types <> derive_Y thm
R4939:4946 operator_types <> derive_Y thm
R4990:4998 Unstar <> unstar_fn def
R5008:5017 type_derivation <> derive_abs constr
R5008:5017 type_derivation <> derive_abs constr
R5028:5038 type_derivation <> derive_gen1 constr
R5028:5038 type_derivation <> derive_gen1 constr
R5049:5052 LamSF_Terms <> lift def
R5083:5092 type_derivation <> derive_app constr
R5083:5092 type_derivation <> derive_app constr
R5102:5109 operator_types <> derive_G thm
R5102:5109 operator_types <> derive_G thm
R5153:5163 type_derivation <> derive_gen1 constr
R5153:5163 type_derivation <> derive_gen1 constr
R5174:5177 LamSF_Terms <> lift def
R5216:5225 type_derivation <> derive_app constr
R5216:5225 type_derivation <> derive_app constr
R5235:5244 type_derivation <> derive_app constr
R5235:5244 type_derivation <> derive_app constr
R5254:5262 operator_types <> derive_DA thm
R5254:5262 operator_types <> derive_DA thm
R5295:5304 Unstar <> abs_A_type thm
R5295:5304 Unstar <> abs_A_type thm
R5315:5324 type_derivation <> derive_app constr
R5315:5324 type_derivation <> derive_app constr
R5334:5343 type_derivation <> derive_app constr
R5334:5343 type_derivation <> derive_app constr
R5353:5361 operator_types <> derive_DK thm
R5353:5361 operator_types <> derive_DK thm
R5393:5402 subject_reduction <> derive_nil thm
R5393:5402 subject_reduction <> derive_nil thm
R5414:5423 Unstar <> abs_K_type thm
R5414:5423 Unstar <> abs_K_type thm
R5445:5454 type_derivation <> derive_app constr
R5445:5454 type_derivation <> derive_app constr
R5464:5471 operator_types <> derive_G thm
R5464:5471 operator_types <> derive_G thm
R5513:5523 type_derivation <> derive_gen1 constr
R5513:5523 type_derivation <> derive_gen1 constr
R5534:5537 LamSF_Terms <> lift def
R5575:5584 type_derivation <> derive_app constr
R5575:5584 type_derivation <> derive_app constr
R5594:5603 type_derivation <> derive_app constr
R5594:5603 type_derivation <> derive_app constr
R5614:5622 operator_types <> derive_DS thm
R5614:5622 operator_types <> derive_DS thm
R5654:5663 subject_reduction <> derive_nil thm
R5654:5663 subject_reduction <> derive_nil thm
R5675:5684 Unstar <> abs_S_type thm
R5675:5684 Unstar <> abs_S_type thm
R5707:5714 operator_types <> derive_I thm
prf 5748:5758 <> unstar_star
R5784:5792 LamSF_reduction <> lamSF_red def
R5817:5819 LamSF_Terms <> Abs constr
R5821:5821 Unstar <> M var
R5795:5797 LamSF_Terms <> App constr
R5807:5810 Components <> star def
R5812:5812 Unstar <> M var
R5799:5804 Unstar <> unstar def
R5772:5777 LamSF_Normal <> normal ind
R5779:5779 Unstar <> M var
R5915:5920 Unstar <> unstar def
R5943:5956 LamSF_Tactics <> transitive_red thm
R5943:5956 LamSF_Tactics <> transitive_red thm
R5967:5989 LamSF_reduction <> preserves_app_lamSF_red thm
R5967:5989 LamSF_reduction <> preserves_app_lamSF_red thm
R6024:6032 Unstar <> unstar_fn def
R6068:6077 Compounds <> factorable def
R6134:6147 LamSF_Tactics <> transitive_red thm
R6134:6147 LamSF_Tactics <> transitive_red thm
R6158:6180 LamSF_reduction <> preserves_app_lamSF_red thm
R6158:6180 LamSF_reduction <> preserves_app_lamSF_red thm
R6191:6198 LamSF_Tactics <> succ_red constr
R6191:6198 LamSF_Tactics <> succ_red constr
R6209:6224 LamSF_reduction <> da_oth_lamSF_red constr
R6209:6224 LamSF_reduction <> da_oth_lamSF_red constr
R6235:6244 Compounds <> factorable def
R6291:6298 LamSF_Tactics <> succ_red constr
R6291:6298 LamSF_Tactics <> succ_red constr
R6309:6324 LamSF_reduction <> dk_oth_lamSF_red constr
R6309:6324 LamSF_reduction <> dk_oth_lamSF_red constr
R6335:6344 Compounds <> factorable def
R6399:6408 Compounds <> factorable def
R6448:6461 LamSF_Tactics <> transitive_red thm
R6448:6461 LamSF_Tactics <> transitive_red thm
R6472:6494 LamSF_reduction <> preserves_app_lamSF_red thm
R6472:6494 LamSF_reduction <> preserves_app_lamSF_red thm
R6505:6512 LamSF_Tactics <> succ_red constr
R6505:6512 LamSF_Tactics <> succ_red constr
R6523:6536 LamSF_reduction <> ds_s_lamSF_red constr
R6523:6536 LamSF_reduction <> ds_s_lamSF_red constr
R6603:6625 LamSF_reduction <> preserves_abs_lamSF_red thm
R6603:6625 LamSF_reduction <> preserves_abs_lamSF_red thm
R6657:6662 Unstar <> unstar def
R6685:6698 LamSF_Tactics <> transitive_red thm
R6685:6698 LamSF_Tactics <> transitive_red thm
R6709:6731 LamSF_reduction <> preserves_app_lamSF_red thm
R6709:6731 LamSF_reduction <> preserves_app_lamSF_red thm
R6766:6774 Unstar <> unstar_fn def
R6810:6819 Compounds <> factorable def
R6876:6889 LamSF_Tactics <> transitive_red thm
R6876:6889 LamSF_Tactics <> transitive_red thm
R6900:6922 LamSF_reduction <> preserves_app_lamSF_red thm
R6900:6922 LamSF_reduction <> preserves_app_lamSF_red thm
R6933:6940 LamSF_Tactics <> succ_red constr
R6933:6940 LamSF_Tactics <> succ_red constr
R6951:6966 LamSF_reduction <> da_oth_lamSF_red constr
R6951:6966 LamSF_reduction <> da_oth_lamSF_red constr
R6977:6986 Compounds <> factorable def
R7033:7040 LamSF_Tactics <> succ_red constr
R7033:7040 LamSF_Tactics <> succ_red constr
R7051:7064 LamSF_reduction <> dk_k_lamSF_red constr
R7051:7064 LamSF_reduction <> dk_k_lamSF_red constr
R7075:7084 Compounds <> factorable def
R7137:7159 LamSF_reduction <> preserves_abs_lamSF_red thm
R7137:7159 LamSF_reduction <> preserves_abs_lamSF_red thm
R7197:7200 LamSF_Terms <> lift def
R7250:7255 Unstar <> unstar def
R7278:7291 LamSF_Tactics <> transitive_red thm
R7278:7291 LamSF_Tactics <> transitive_red thm
R7302:7324 LamSF_reduction <> preserves_app_lamSF_red thm
R7302:7324 LamSF_reduction <> preserves_app_lamSF_red thm
R7359:7367 Unstar <> unstar_fn def
R7403:7412 Compounds <> factorable def
R7469:7482 LamSF_Tactics <> transitive_red thm
R7469:7482 LamSF_Tactics <> transitive_red thm
R7493:7515 LamSF_reduction <> preserves_app_lamSF_red thm
R7493:7515 LamSF_reduction <> preserves_app_lamSF_red thm
R7526:7533 LamSF_Tactics <> succ_red constr
R7526:7533 LamSF_Tactics <> succ_red constr
R7544:7559 LamSF_reduction <> da_oth_lamSF_red constr
R7544:7559 LamSF_reduction <> da_oth_lamSF_red constr
R7570:7579 Compounds <> factorable def
R7626:7633 LamSF_Tactics <> succ_red constr
R7626:7633 LamSF_Tactics <> succ_red constr
R7644:7657 LamSF_reduction <> dk_k_lamSF_red constr
R7644:7657 LamSF_reduction <> dk_k_lamSF_red constr
R7710:7715 Unstar <> unstar def
R7750:7758 Unstar <> unstar_fn def
R7794:7803 Compounds <> factorable def
R7860:7873 LamSF_Tactics <> transitive_red thm
R7860:7873 LamSF_Tactics <> transitive_red thm
R7884:7906 LamSF_reduction <> preserves_app_lamSF_red thm
R7884:7906 LamSF_reduction <> preserves_app_lamSF_red thm
R7918:7925 LamSF_Tactics <> succ_red constr
R7956:7978 LamSF_reduction <> preserves_abs_lamSF_red thm
R7956:7978 LamSF_reduction <> preserves_abs_lamSF_red thm
R7989:8002 LamSF_Tactics <> transitive_red thm
R7989:8002 LamSF_Tactics <> transitive_red thm
R8013:8035 LamSF_reduction <> preserves_app_lamSF_red thm
R8013:8035 LamSF_reduction <> preserves_app_lamSF_red thm
R8055:8060 Unstar <> unstar def
R8078:8081 LamSF_Terms <> lift def
R8112:8130 LamSF_Substitution_term <> subst_rec_lift_rec2 thm
R8112:8130 LamSF_Substitution_term <> subst_rec_lift_rec2 thm
R8193:8198 Unstar <> unstar def
R8221:8234 LamSF_Tactics <> transitive_red thm
R8221:8234 LamSF_Tactics <> transitive_red thm
R8245:8267 LamSF_reduction <> preserves_app_lamSF_red thm
R8245:8267 LamSF_reduction <> preserves_app_lamSF_red thm
R8302:8310 Unstar <> unstar_fn def
R8346:8355 Compounds <> factorable def
R8412:8425 LamSF_Tactics <> transitive_red thm
R8412:8425 LamSF_Tactics <> transitive_red thm
R8436:8458 LamSF_reduction <> preserves_app_lamSF_red thm
R8436:8458 LamSF_reduction <> preserves_app_lamSF_red thm
R8469:8476 LamSF_Tactics <> succ_red constr
R8469:8476 LamSF_Tactics <> succ_red constr
R8487:8502 LamSF_reduction <> da_oth_lamSF_red constr
R8487:8502 LamSF_reduction <> da_oth_lamSF_red constr
R8513:8522 Compounds <> factorable def
R8569:8576 LamSF_Tactics <> succ_red constr
R8569:8576 LamSF_Tactics <> succ_red constr
R8587:8602 LamSF_reduction <> dk_oth_lamSF_red constr
R8587:8602 LamSF_reduction <> dk_oth_lamSF_red constr
R8613:8622 Compounds <> factorable def
R8677:8686 Compounds <> factorable def
R8718:8731 LamSF_Tactics <> transitive_red thm
R8718:8731 LamSF_Tactics <> transitive_red thm
R8742:8764 LamSF_reduction <> preserves_app_lamSF_red thm
R8742:8764 LamSF_reduction <> preserves_app_lamSF_red thm
R8782:8789 LamSF_Tactics <> succ_red constr
R8782:8789 LamSF_Tactics <> succ_red constr
R8800:8813 LamSF_reduction <> ds_s_lamSF_red constr
R8800:8813 LamSF_reduction <> ds_s_lamSF_red constr
R8886:8908 LamSF_reduction <> preserves_abs_lamSF_red thm
R8886:8908 LamSF_reduction <> preserves_abs_lamSF_red thm
R8920:8937 LamSF_Substitution_term <> subst_rec_lift_rec thm
R8920:8937 LamSF_Substitution_term <> subst_rec_lift_rec thm
R8959:8972 LamSF_Tactics <> transitive_red thm
R8959:8972 LamSF_Tactics <> transitive_red thm
R8983:9005 LamSF_reduction <> preserves_app_lamSF_red thm
R8983:9005 LamSF_reduction <> preserves_app_lamSF_red thm
R9029:9032 LamSF_Terms <> lift def
R9070:9088 LamSF_Substitution_term <> subst_rec_lift_rec2 thm
R9070:9088 LamSF_Substitution_term <> subst_rec_lift_rec2 thm
R9070:9088 LamSF_Substitution_term <> subst_rec_lift_rec2 thm
R9070:9088 LamSF_Substitution_term <> subst_rec_lift_rec2 thm