blob: 9ad9bc21e4894a620b49521d0b2f76365e775d43 (
plain)
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
391
392
393
394
|
1 size0nil
2 nilP
3 size_behead
4 size_ncons
5 size_nseq
6 cat0s
7 cat1s
8 cat_cons
9 cat_nseq
10 cats0
11 catA
12 size_cat
13 rcons_cons
14 cats1
15 lastI
16 last_cons
17 size_rcons
18 size_belast
19 last_cat
20 last_rcons
21 belast_cat
22 belast_rcons
23 cat_rcons
24 rcons_cat
25 lastP
26 last_ind
27 nth0
28 nth_default
29 nth_nil
30 last_nth
31 nth_last
32 nth_behead
33 nth_cat
34 nth_rcons
35 nth_ncons
36 nth_nseq
37 eq_from_nth
38 size_set_nth
39 set_nth_nil
40 nth_set_nth
41 set_set_nth
42 count_filter
43 has_count
44 count_size
45 all_count
46 filter_all
47 all_filterP
48 filter_id
49 has_find
50 find_size
51 find_cat
52 has_nil
53 has_seq1
54 has_seqb
55 all_nil
56 all_seq1
57 nth_find
58 before_find
59 filter_cat
60 filter_rcons
61 count_cat
62 has_cat
63 has_rcons
64 all_cat
65 all_rcons
66 eq_find
67 eq_filter
68 eq_count
69 eq_has
70 eq_all
71 sub_find
72 sub_has
73 sub_count
74 sub_all
75 filter_pred0
76 filter_predT
77 filter_predI
78 count_pred0
79 count_predT
80 count_predUI
81 count_predC
82 has_pred0
83 has_predT
84 has_predC
85 has_predU
86 all_pred0
87 all_predT
88 all_predC
89 all_predI
90 drop_behead
91 drop0
92 drop1
93 drop_oversize
94 drop_size
95 drop_cons
96 size_drop
97 drop_cat
98 drop_size_cat
99 nconsK
100 take0
101 take_oversize
102 take_size
103 take_cons
104 drop_rcons
105 cat_take_drop
106 size_takel
107 size_take
108 take_cat
109 take_size_cat
110 takel_cat
111 nth_drop
112 nth_take
113 drop_nth
114 take_nth
115 rot0
116 size_rot
117 rot_oversize
118 rot_size
119 has_rot
120 rot_size_cat
121 rotK
122 rot_inj
123 rot1_cons
124 catrev_catl
125 catrev_catr
126 catrevE
127 rev_cons
128 size_rev
129 rev_cat
130 rev_rcons
131 revK
132 nth_rev
133 eqseqP
134 eqseqE
135 eqseq_cons
136 eqseq_cat
137 eqseq_rcons
138 has_filter
139 size_eq0
140 in_cons
141 in_nil
142 mem_seq1
143 mem_seq2
144 mem_seq3
145 mem_seq4
146 mem_cat
147 mem_rcons
148 mem_head
149 mem_last
150 mem_behead
151 mem_belast
152 mem_nth
153 mem_take
154 mem_drop
155 mem_rev
156 hasP
157 hasPn
158 allP
159 allPn
160 mem_filter
161 eq_in_filter
162 eq_in_find
163 eq_in_count
164 eq_in_all
165 eq_in_has
166 eq_has_r
167 eq_all_r
168 has_sym
169 has_pred1
170 all_pred1P
171 all_pred1_constant
172 all_pred1_nseq
173 constant_nseq
174 constantP
175 cons_uniq
176 cat_uniq
177 uniq_catC
178 uniq_catCA
179 rcons_uniq
180 filter_uniq
181 rot_uniq
182 rev_uniq
183 count_uniq_mem
184 filter_pred1_uniq
185 size_undup
186 mem_undup
187 undup_uniq
188 undup_id
189 ltn_size_undup
190 filter_undup
191 index_size
192 index_mem
193 nth_index
194 index_cat
195 index_uniq
196 index_head
197 index_last
198 nth_uniq
199 mem_rot
200 eqseq_rot
201 rot_to
202 nthP
203 has_nthP
204 all_nthP
205 set_nth_default
206 headI
207 nth_incr_nth
208 size_incr_nth
209 perm_eqP
210 perm_eq_refl
211 perm_eq_sym
212 perm_eq_trans
213 perm_eqlE
214 perm_eqlP
215 perm_eqrP
216 perm_catC
217 perm_cat2l
218 perm_cons
219 perm_cat2r
220 perm_catAC
221 perm_catCA
222 perm_rcons
223 perm_rot
224 perm_rotr
225 perm_filterC
226 perm_eq_mem
227 perm_eq_size
228 perm_eq_small
229 uniq_leq_size
230 leq_size_uniq
231 uniq_size_uniq
232 leq_size_perm
233 perm_uniq
234 perm_eq_uniq
235 uniq_perm_eq
236 count_mem_uniq
237 catCA_perm_ind
238 catCA_perm_subst
239 size_rotr
240 mem_rotr
241 rotr_size_cat
242 rotr1_rcons
243 has_rotr
244 rotr_uniq
245 rotrK
246 rotr_inj
247 rev_rot
248 rev_rotr
249 rot_addn
250 rotS
251 rot_add_mod
252 rot_rot
253 rot_rotr
254 rotr_rotr
255 mask_false
256 mask_true
257 mask0
258 mask1
259 mask_cons
260 size_mask
261 mask_cat
262 has_mask_cons
263 has_mask
264 mask_rot
265 mem_mask_cons
266 mem_mask
267 mask_uniq
268 mem_mask_rot
269 sub0seq
270 subseq0
271 subseqP
272 subseq_trans
273 subseq_refl
274 cat_subseq
275 prefix_subseq
276 suffix_subseq
277 mem_subseq
278 sub1seq
279 size_subseq
280 size_subseq_leqif
281 subseq_cons
282 subseq_rcons
283 subseq_uniq
284 rem_id
285 perm_to_rem
286 size_rem
287 rem_subseq
288 rem_uniq
289 mem_rem
290 rem_filter
291 mem_rem_uniq
292 map_cons
293 map_nseq
294 map_cat
295 size_map
296 behead_map
297 nth_map
298 map_rcons
299 last_map
300 belast_map
301 filter_map
302 find_map
303 has_map
304 all_map
305 count_map
306 map_take
307 map_drop
308 map_rot
309 map_rotr
310 map_rev
311 map_mask
312 inj_map
313 filter_mask
314 filter_subseq
315 subseq_filter
316 subseq_uniqP
317 perm_to_subseq
318 map_f
319 mapP
320 map_uniq
321 map_inj_in_uniq
322 map_subseq
323 nth_index_map
324 perm_map
325 mem_map
326 index_map
327 map_inj_uniq
328 map_of_seq
329 map_id
330 eq_map
331 map_comp
332 mapK
333 eq_in_map
334 map_id_in
335 map_pK
336 size_pmap
337 pmapS_filter
338 pmap_filter
339 eq_pmap
340 mem_pmap
341 can2_mem_pmap
342 pmap_uniq
343 size_pmap_sub
344 mem_pmap_sub
345 pmap_sub_uniq
346 size_iota
347 iota_add
348 iota_addl
349 nth_iota
350 mem_iota
351 iota_uniq
352 size_mkseq
353 eq_mkseq
354 nth_mkseq
355 mkseq_nth
356 mkseq_uniq
357 perm_eq_iotaP
358 foldr_cat
359 foldr_map
360 sumn_nseq
361 sumn_cat
362 natnseq0P
363 foldl_rev
364 foldl_cat
365 size_pairmap
366 pairmap_cat
367 nth_pairmap
368 size_scanl
369 scanl_cat
370 nth_scanl
371 scanlK
372 pairmapK
373 zip_unzip
374 unzip1_zip
375 unzip2_zip
376 size1_zip
377 size2_zip
378 size_zip
379 zip_cat
380 nth_zip
381 nth_zip_cond
382 zip_rcons
383 rev_zip
384 size_flatten
385 flatten_cat
386 flattenK
387 reshapeKr
388 reshapeKl
389 size_allpairs
390 allpairs_cat
391 allpairsP
392 mem_allpairs
393 allpairs_catr
394 allpairs_uniq
|
