| Name | Category | Theorems |
|---|
Forall đ | MathDef | 6 mathmath: forall_map_iff, forall_cons, Poly.sumsq_eq_zero, forall_iff_forall_mem, forall_zipWith, forall_append
|
andM đ | CompOp | â |
chooseX đ | CompOp | â |
dedup đ | CompOp | 35 mathmath: Disjoint.dedup_append, dedup_nil, ArithmeticFunction.cardDistinctFactors_apply, sum_map_count_dedup_eq_length, dedup_eq_self, Perm.dedup, dedup_cons_of_notMem, replicate_dedup, toFinset_eq_iff_perm_dedup, dedup_cons, Subset.dedup_append_right, nodup_dedup, card_toFinset, tail_dedup, mem_dedup, headI_dedup, Multiset.coe_dedup, dedup_cons', count_dedup, toFinset_val, subset_dedup, Subset.dedup_append_left, dedup_append, dedup_cons_of_mem, dedup_sublist, dedup_eq_cons, Nodup.dedup, sum_map_count_dedup_filter_eq_countP, dedup_sym2, Disjoint.union_eq, Pairwise.destutter_eq_dedup, dedup_eq_nil, dedup_map_of_injective, dedup_subset, dedup_idem
|
destutter đ | CompOp | 20 mathmath: length_destutter_ne_le_length_destutter_cons, destutter_idem, destutter_sublist, destutter_is_chain', IsChain.length_le_length_destutter, destutter_eq_nil, destutter_nil, destutter_singleton, destutter_eq_self_iff, map_destutter, isChain_destutter, IsChain.length_le_length_destutter_ne, length_destutter_le_length_destutter_cons, destutter_pair, Pairwise.destutter_eq_dedup, destutter_cons', destutter_of_isChain, destutter_cons_cons, destutter_of_chain', map_destutter_ne
|
destutter' đ | CompOp | 19 mathmath: mem_destutter', length_destutter'_cotrans_ge, destutter'_is_chain', destutter'_cons_neg, isChain_cons_destutter'_of_rel, destutter'_nil, destutter'_sublist, length_destutter'_congr, isChain_destutter', destutter'_cons_pos, destutter'_eq_self_iff, le_length_destutter'_cons, destutter'_is_chain, destutter'_singleton, destutter'_cons, destutter_cons', destutter'_of_isChain_cons, destutter_cons_cons, destutter'_of_chain
|
| đ | CompOp | â |
findM đ | CompOp | â |
findM?' đ | CompOp | â |
foldlIdxM đ | CompOp | â |
foldrIdxM đ | CompOp | â |
getI đ | CompOp | 15 mathmath: Nat.testBit_eq_inth, getI_append_right, getI_nil, getI_cons_succ, getI_append, getD_default_eq_getI, getI_zero_eq_headI, getI_eq_iget_getElem?, getI_eq_default, getI_eq_getElem?_getD, Set.range_list_getI, getI_eq_getElem, Primrec.list_getI, Turing.ListBlank.nth_mk, getI_cons_zero
|
getLastI đ | CompOp | 2 mathmath: getLastI_eq_getLast?_getD, getLastI_eq_getLast?
|
headI đ | CompOp | 23 mathmath: headI_mul_tail_prod_of_ne_nil, Turing.PointedMap.headI_map, Turing.ToPartrec.Code.pred_eval, tail_sum, Turing.ToPartrec.Code.head_eval, headI_add_tail_sum_of_ne_nil, getI_zero_eq_headI, headI_nil, headI_cons, Turing.PartrecToTM2.head_stack_ok, tail_dedup, Primrec.list_headI, Turing.ToPartrec.Code.cons_eval, Turing.ListBlank.head_mk, headI_dedup, headI_le_sum, Turing.ToPartrec.Code.succ_eval, Turing.PartrecToTM2.pred_ok, Turing.ToPartrec.Code.fix_eval, Nat.bodd_eq_bits_head, Turing.ToPartrec.Code.case_eval, Turing.PartrecToTM2.head_main_ok, headI_add_tail_sum
|
instSDiffOfDecidableEq_mathlib đ | CompOp | â |
instSProd đ | CompOp | 7 mathmath: Multiset.coe_product, product_cons, product_nil, nil_product, mem_product, length_product, Nodup.product
|
iterate đ | CompOp | 9 mathmath: iterate_add, getElem?_iterate, range_map_iterate, take_iterate, iterate_eq_nil, mem_iterate, iterateTR_loop_eq, iterate_eq_iterateTR, length_iterate
|
iterateTR đ | CompOp | 1 mathmath: iterate_eq_iterateTR
|
mapAccumr đ | CompOp | 2 mathmath: length_mapAccumr, mapAccumr_eq_foldr
|
mapAccumrâ đ | CompOp | 2 mathmath: length_mapAccumrâ, mapAccumrâ_eq_foldr
|
mapAsyncChunked đ | CompOp | â |
mapDiagM' đ | CompOp | â |
mapIdxM' đ | CompOp | 1 mathmath: mapIdxM'_eq_mapIdxM
|
mapIdxMAux' đ | CompOp | 1 mathmath: mapIdxMAux'_eq_mapIdxMGo
|
mapâLeft đ | CompOp | 3 mathmath: mapâLeft_nil_right, mapâLeft_eq_mapâLeft', mapâLeft_eq_zipWith
|
mapâLeft' đ | CompOp | 2 mathmath: mapâLeft'_nil_right, mapâLeft_eq_mapâLeft'
|
mapâRight đ | CompOp | 6 mathmath: mapâRight_eq_zipWith, mapâRight_nil_left, mapâRight_nil_cons, mapâRight_eq_mapâRight', mapâRight_nil_right, mapâRight_cons_cons
|
mapâRight' đ | CompOp | 5 mathmath: mapâRight'_nil_right, mapâRight'_cons_cons, mapâRight'_nil_cons, mapâRight_eq_mapâRight', mapâRight'_nil_left
|
orM đ | CompOp | â |
permutations đ | CompOp | 14 mathmath: nodup_permutations, nodup_permutations_iff, permutationsAux_cons, Multiset.lists_coe, map_permutations, length_permutations, permutations_perm_permutations', permutations_append, mem_permutations_of_perm_lemma, mem_permutations, permutations_nil, Perm.permutations, permutations_take_two, perm_permutations_iff
|
permutations' đ | CompOp | 5 mathmath: map_permutations', perm_permutations'_iff, permutations_perm_permutations', mem_permutations', Perm.permutations'
|
permutations'Aux đ | CompOp | 8 mathmath: count_permutations'Aux_self, nodup_permutations'Aux_of_notMem, nodup_permutations'Aux_iff, length_permutations'Aux, map_map_permutations'Aux, injective_permutations'Aux, permutations'Aux_eq_permutationsAux2, perm_permutations'Aux_comm
|
permutationsAux đ | CompOp | 7 mathmath: permutationsAux_nil, permutationsAux_cons, mem_permutationsAux_of_perm, permutations_append, map_permutationsAux, length_permutationsAux, permutationsAux_append
|
permutationsAux2 đ | CompOp | 18 mathmath: permutationsAux2_snd_eq, map_permutationsAux2, permutationsAux2_fst, permutationsAux2_comp_append, mem_permutationsAux2, length_foldr_permutationsAux2', permutationsAux_cons, mem_permutationsAux2', mem_foldr_permutationsAux2, permutationsAux2_append, foldr_permutationsAux2, permutationsAux2_snd_cons, length_foldr_permutationsAux2, permutations'Aux_eq_permutationsAux2, length_permutationsAux2, map_map_permutationsAux2, permutationsAux2_snd_nil, map_permutationsAux2'
|
replaceIf đ | CompOp | â |
takeI đ | CompOp | 5 mathmath: takeI_nil, takeI_eq_take, takeI_left', takeI_left, takeI_length
|
zipWith3 đ | CompOp | 5 mathmath: zipWith3_same_right, zipWith_zipWith_left, zipWith_zipWith_right, zipWith3_same_mid, zipWith3_same_left
|
zipWith4 đ | CompOp | â |
zipWith5 đ | CompOp | â |