| Metric | Count |
|---|
DefinitionsChain, Chain', Disjoint, Forall₂, IsChain, Subperm, after, allSome, all₂, bagInter, countBefore, countPBefore, go, diff, dropInfix?, go, dropPrefix?, dropSlice, dropSliceTR, go, dropSuffix?, eraseDup, extractP, go, fillNones, findIdxNth, go, findIdxs, findIdxsValues, foldlIdx, foldrIdx, foldrIdxTR, forDiagM, getRest, idxOfNth, idxsOf, indexesOf, indexsValues, inits, initsTR, insertP, loop, instDecidableForall₂, instDecidableIsChainOfDecidableRel, go, instInterOfBEq_batteries, instUnionOfBEq_batteries, inter, isSubperm, lookmap, go, mapDiagM, go, mapWithComplement, mapWithPrefixSuffix, mapWithPrefixSuffixAux, modifyLast, go, next?, ofFnNthVal, partialProds, partialSums, prod, product, productTR, pwFilter, replaceF, replaceFTR, go, revzip, rotate, rotate', scanAuxM, go, sections, sectionsTR, go, sigma, sigmaTR, splitAtD, go, splitOn, splitOnP, go, splitOnPTR, go, sublists, sublists', sublistsFast, tails, tailsTR, go, takeD, takeDTR, go, takeList, takeListTR, go, takeWhile₂, takeWhile₂TR, go, toChunks, go, toChunksAux, transpose, go, pop, traverse, union, zipLeft, zipLeft', zipRight, zipRight', zipWithLeft, zipWithLeft', zipWithLeft'TR, go, zipWithLeftTR, go, zipWithRight, zipWithRight', zipWith₃, zipWith₄, zipWith₅, «term_<+~_» | 125 |
Theoremscons, nil, all₂_eq_true, dropSlice_eq_dropSliceTR, dropSlice_zero₂, foldrIdx_eq_foldrIdxTR, forall₂_cons, headD_eq_head?, inits_eq_initsTR, isChain_cons_cons, product_eq_productTR, replaceF_eq_replaceFTR, sections_eq_nil_of_isEmpty, sections_eq_sectionsTR, sigma_eq_sigmaTR, splitOnP_eq_splitOnPTR, sublists_eq_sublistsFast, tails_eq_tailsTR, takeDTR_go_eq, takeD_eq_takeDTR, takeD_nil, takeD_succ, takeD_zero, takeList_eq_takeListTR, takeWhile₂_eq_takeWhile₂TR, zipWithLeft'_eq_zipWithLeft'TR, zipWithLeft_eq_zipWithLeftTR | 27 |
| Total | 152 |
| Name | Category | Theorems |
|---|
Chain 📖 | MathDef | 2 mathmath: Chain.cons, Chain.nil
|
Chain' 📖 | MathDef | — |
Disjoint 📖 | MathDef | 22 mathmath: disjoint_iff_ne, disjoint_of_subset_left, disjoint_of_disjoint_cons_right, disjoint_left, disjoint_take_drop, disjoint_symm, disjoint_of_disjoint_cons_left, disjoint_comm, singleton_disjoint, disjoint_of_disjoint_append_left_left, disjoint_singleton, disjoint_append_right, disjoint_of_disjoint_append_left_right, disjoint_nil_right, disjoint_right, disjoint_append_left, disjoint_of_disjoint_append_right_right, disjoint_cons_right, disjoint_cons_left, disjoint_nil_left, disjoint_of_subset_right, disjoint_of_disjoint_append_right_left
|
Forall₂ 📖 | CompData | 1 math, 1 bridgemath: forall₂_cons
bridge: all₂_eq_true
|
IsChain 📖 | CompData | 23 mathmath: isChain_idxsOf, isChain_lt_range', isChain_cons_of_isChain_cons_cons, IsChain.cons_of_imp, isChain_of_isChain_cons_cons, Chain.imp', IsChain.of_cons, chain_lt_range', isChain_of_isChain_cons, Chain.imp, IsChain.cons_of_imp_of_cons, isChain_cons_cons, isChain_range', isChain_findIdxs, chain_cons, IsChain.cons_of_imp_of_imp, isChain_iff_getElem, chain_of_chain_cons, Pairwise.isChain, chain_succ_range', Pairwise.chain, isChain_iff_pairwise, IsChain.imp
|
Subperm 📖 | MathDef | 26 math, 1 bridgemath: Subperm.cons_left, subperm_append_left, subperm_of_subset, erase_subperm, singleton_subperm_iff, Subperm.filter, erase_cons_subperm_cons_erase, Subperm.erase, Subperm.cons_right, Subperm.exists_of_length_lt, subperm_nil, Subperm.trans, subperm_append_right, Perm.subperm, subperm_cons_erase, Subperm.cons_self, Subperm.refl, Perm.subperm_right, subperm_cons, nil_subperm, Sublist.subperm, Perm.subperm_left, Subperm.diff_right, cons_subperm_of_not_mem_of_mem, subperm_cons_diff, subperm_ext_iff
bridge: isSubperm_iff
|
after 📖 | CompOp | — |
allSome 📖 | CompOp | — |
all₂ 📖 | CompOp | 1 bridgebridge: all₂_eq_true
|
bagInter 📖 | CompOp | — |
countBefore 📖 | CompOp | 18 mathmath: countBefore_zero, snd_idxToSigmaCount, countBefore_nil, idxOfNth_countBefore_of_lt_length_of_beq, countBefore_cons, Perm.coe_idxBij, countBefore_cons_succ, countBefore_le_count, countBefore_idxOfNth_of_lt_count, idxOfNth_countBefore_getElem, countBefore_eq_count_take, countBefore_lt_count_getElem, countBefore_cons_succ_of_not_beq, coe_idxInj, countBefore_of_ge_length, countBefore_cons_succ_of_beq, countBefore_lt_count_of_lt_length_of_beq, coe_snd_idxToSigmaCount
|
countPBefore 📖 | CompOp | 16 mathmath: findIdxNth_countPBefore_of_lt_length_of_pos, countPBefore_le_countP, countPBefore_zero, countPBefore_cons, countPBefore_cons_succ_of_neg, countPBefore_cons_succ, countPBefore_mono, countPBefore_of_ge_length, countPBefore_cons_succ_of_pos, countPBefore_findIdxNth_of_lt_countP, countPBefore_cons_zero, countPBefore_nil, countPBefore_succ, countPBefore_lt_countP_of_lt_length_of_pos, countPBefore_length, countPBefore_eq_countP_take
|
diff 📖 | CompOp | 22 mathmath: diff_eq_foldl, diff_sublist, nil_diff, diff_cons_right, diff_append, Perm.diff, mem_diff_of_mem, Perm.diff_right, cons_diff_of_mem, diff_cons, diff_subset, diff_nil, Sublist.erase_diff_erase_sublist, subperm_append_diff_self_of_count_le, Perm.diff_left, diff_erase, Subperm.diff_right, Sublist.diff_right, cons_diff_of_not_mem, cons_diff, subperm_cons_diff, subset_cons_diff
|
dropInfix? 📖 | CompOp | 2 mathmath: dropInfix?_nil, dropInfix?_eq_some_iff
|
dropPrefix? 📖 | CompOp | 3 mathmath: dropPrefix?_append_of_beq, dropPrefix?_nil, dropPrefix?_eq_some_iff
|
dropSlice 📖 | CompOp | 2 mathmath: dropSlice_zero₂, dropSlice_eq_dropSliceTR
|
dropSliceTR 📖 | CompOp | 1 mathmath: dropSlice_eq_dropSliceTR
|
dropSuffix? 📖 | CompOp | 2 mathmath: dropSuffix?_eq_some_iff, dropSuffix?_nil
|
eraseDup 📖 | CompOp | — |
| 📖 | CompOp | 1 mathmath: extractP_eq_find?_eraseP
|
fillNones 📖 | CompOp | — |
findIdxNth 📖 | CompOp | 28 mathmath: findIdxNth_countPBefore_of_lt_length_of_pos, findIdxNth_cons_succ_of_pos, findIdxNth_le_findIdxNth_iff, findIdxNth_lt_length_of_lt_countP, findIdxNth_eq_findIdxNth_iff, findIdxNth_le_length, getElem_findIdxs_eq_findIdxNth, findIdxNth_mono, findIdxNth_nil, pos_iff_exists_findIdxNth, findIdxNth_zero, findIdxNth_eq_findIdxNth_iff_of_left_lt_countP, getElem_findIdxs_eq_findIdxNth_add, findIdxNth_eq_findIdxNth_iff_of_right_lt_countP, findIdxNth_cons, findIdxNth_lt_findIdxNth_iff, countPBefore_findIdxNth_of_lt_countP, findIdxNth_cons_zero, findIdxNth_lt_findIdxNth_iff_of_lt_countP, findIdxNth_eq_length_iff, findIdxNth_lt_length_iff, findIdxNth_cons_succ, findIdxNth_cons_of_neg, findIdxNth_cons_of_pos, findIdxNth_cons_zero_of_pos, findIdxNth_eq_length_of_ge_countP, findIdxNth_eq_findIdxNth_of_ge_countP_ge_countP, pos_findIdxNth_getElem
|
findIdxs 📖 | CompOp | 31 mathmath: findIdxs_eq_nil_iff, getElem_getElem_findIdxs_sub, mem_findIdxs_iff_getElem_sub_pos, findIdx_mem_findIdxs, mem_findIdxs_iff_pos_getElem, findIdx_add_mem_findIdxs, idxsOf_map, getElem_findIdxs_eq_findIdxNth, unzip_findIdxsValues, pairwise_findIdxs, findIdxs_map, findIdxs_take, isChain_findIdxs, findIdxs_start, getElem_findIdxs_eq_findIdxNth_add, getElem_zero_findIdxs_eq_findIdx_add, getElem_filter_eq_getElem_getElem_findIdxs_sub, findIdxsValues_eq_zip_filter_findIdxs, getElem_zero_findIdxs_eq_findIdx, le_getElem_findIdxs, mem_findIdxs_iff_exists_getElem_pos, findIdxs_nil, length_findIdxs, getElem_filter_eq_getElem_getElem_findIdxs, getElem_findIdxs_lt, findIdxs_eq_filterMap_zipIdx, findIdxs_cons, nodup_findIdxs, findIdxs_singleton, findIdxs_append, getElem_getElem_findIdxs
|
findIdxsValues 📖 | CompOp | 2 mathmath: unzip_findIdxsValues, findIdxsValues_eq_zip_filter_findIdxs
|
foldlIdx 📖 | CompOp | 5 mathmath: foldlIdx_start, foldlIdx_nil, foldlIdx_cons, foldlIdx_eq_foldl_zipIdx, foldlIdx_const
|
foldrIdx 📖 | CompOp | 6 mathmath: foldrIdx_eq_foldr_zipIdx, foldrIdx_start, foldrIdx_eq_foldrIdxTR, foldrIdx_cons, foldrIdx_const, foldrIdx_nil
|
foldrIdxTR 📖 | CompOp | 1 mathmath: foldrIdx_eq_foldrIdxTR
|
forDiagM 📖 | CompOp | — |
getRest 📖 | CompOp | — |
idxOfNth 📖 | CompOp | 32 mathmath: idxOfNth_cons_succ_of_beq, idxOfNth_eq_idxOfNth_iff_of_right_lt_count, idxOfNth_lt_length_iff, getElem_idxOf_eq_idxOfNth_add, idxOfNth_lt_length_of_lt_count, idxOfNth_cons_succ, idxOfNth_eq_length_of_ge_count, idxOfNth_lt_idxOfNth_iff_of_lt_count, idxOfNth_eq_idxOfNth_iff_of_left_lt_count, idxOfNth_eq_length_iff, getElem_idxOfNth_beq, beq_iff_exists_findIdxNth, idxOfNth_cons_zero_of_beq, idxOfNth_countBefore_of_lt_length_of_beq, idxOfNth_cons_zero, idxOfNth_eq_idxOfNth_of_ge_countP_ge_countP, Perm.coe_idxBij, idxOfNth_eq_idxOfNth_iff, getElem_idxOf_eq_idxOfNth, idxOfNth_mono, countBefore_idxOfNth_of_lt_count, idxOfNth_cons_of_beq, idxOfNth_zero, idxOfNth_countBefore_getElem, getElem_idxOfNth_eq, idxOfNth_cons, idxOfNth_lt_idxOfNth_iff, coe_idxInj, idxOfNth_cons_of_not_beq, idxOfNth_le_length, coe_sigmaCountToIdx, idxOfNth_nil
|
idxsOf 📖 | CompOp | 28 mathmath: isChain_idxsOf, getElem_idxOf_eq_idxOfNth_add, le_getElem_idxsOf, getElem_getElem_idxsOf, idxsOf_map, pairwise_idxsOf, getElem_zero_idxsOf_eq_idxOf, getElem_getElem_idxsOf_of_lawful, nodup_idxsOf, mem_idxsOf_iff_getElem_sub_pos, getElem_idxOf_eq_idxOfNth, mem_idxsOf_getElem, getElem_idxsOf_lt, length_idxsOf, idxsOf_take, getElem_getElem_idxsOf_sub, idxsOf_append, idxsOf_nil, idxOf_mem_idxsOf, idxsOf_start, mem_idxsOf_iff_exists_getElem_pos, getElem_getElem_idxsOf_sub_of_lawful, idxOf_add_mem_idxsOf, idxsOf_eq_nil_iff, idxsOf_eq_filterMap_zipIdx, idxsOf_cons, mem_idxsOf_iff_getElem_pos, getElem_zero_idxsOf_eq_idxOf_add
|
indexesOf 📖 | CompOp | — |
indexsValues 📖 | CompOp | — |
inits 📖 | CompOp | 1 mathmath: inits_eq_initsTR
|
initsTR 📖 | CompOp | 1 mathmath: inits_eq_initsTR
|
insertP 📖 | CompOp | 8 mathmath: length_insertP, insertP_cons_neg, mem_insertP, insertP_nil, perm_insertP, insertP_loop, Perm.insertP, insertP_cons_pos
|
instDecidableForall₂ 📖 | CompOp | — |
instDecidableIsChainOfDecidableRel 📖 | CompOp | — |
instInterOfBEq_batteries 📖 | CompOp | 5 mathmath: inter_def, Perm.inter_right, Perm.inter_left, mem_inter_iff, Perm.inter
|
instUnionOfBEq_batteries 📖 | CompOp | 7 mathmath: nil_union, Perm.union_right, union_def, mem_union_iff, cons_union, Perm.union_left, Perm.union
|
inter 📖 | CompOp | — |
isSubperm 📖 | CompOp | 1 bridgebridge: isSubperm_iff
|
lookmap 📖 | CompOp | — |
mapDiagM 📖 | CompOp | — |
mapWithComplement 📖 | CompOp | — |
mapWithPrefixSuffix 📖 | CompOp | — |
mapWithPrefixSuffixAux 📖 | CompOp | — |
modifyLast 📖 | CompOp | — |
next? 📖 | CompOp | 3 mathmath: Batteries.RBNode.Stream.next?_toList, next?_nil, next?_cons
|
ofFnNthVal 📖 | CompOp | — |
partialProds 📖 | CompOp | 7 mathmath: partialProds_append, partialProds_cons, getElem_partialProds, partialProds_nil, getElem?_partialProds, take_partialProds, length_partialProds
|
partialSums 📖 | CompOp | 10 mathmath: partialSums_cons, getElem?_partialSums, length_flatten_mem_partialSums_map_length, length_partialSums, take_partialSums, partialSums_nil, partialSums_append, getElem_flatten_aux₁, getElem_flatten_aux₂, getElem_partialSums
|
prod 📖 | CompOp | 14 mathmath: partialProds_append, prod_append, prod_flatten, prod_eq_foldl, getElem_partialProds, getElem?_partialProds, prod_one_cons, prod_concat, prod_singleton, prod_pair, prod_nil, prod_eq_foldr, Fin.prod_eq_prod_map_finRange, prod_cons
|
product 📖 | CompOp | 2 mathmath: pair_mem_product, product_eq_productTR
|
productTR 📖 | CompOp | 1 mathmath: product_eq_productTR
|
pwFilter 📖 | CompOp | 9 mathmath: pwFilter_cons_of_pos, pwFilter_subset, pwFilter_idem, pairwise_pwFilter, pwFilter_cons_of_neg, pwFilter_sublist, pwFilter_nil, pwFilter_eq_self, pwFilter_map
|
replaceF 📖 | CompOp | 11 mathmath: replaceF_of_forall_none, replaceF_eq_replaceFTR, replaceF_nil, replaceF_cons_of_some, Batteries.AssocList.toList_modify, replaceF_cons_of_none, Batteries.AssocList.toList_replace, replaceF_cons, exists_or_eq_self_of_replaceF, exists_of_replaceF, length_replaceF
|
replaceFTR 📖 | CompOp | 1 mathmath: replaceF_eq_replaceFTR
|
revzip 📖 | CompOp | — |
rotate 📖 | CompOp | — |
rotate' 📖 | CompOp | — |
scanAuxM 📖 | CompOp | — |
sections 📖 | CompOp | 2 mathmath: sections_eq_nil_of_isEmpty, sections_eq_sectionsTR
|
sectionsTR 📖 | CompOp | 1 mathmath: sections_eq_sectionsTR
|
sigma 📖 | CompOp | 1 mathmath: sigma_eq_sigmaTR
|
sigmaTR 📖 | CompOp | 1 mathmath: sigma_eq_sigmaTR
|
splitAtD 📖 | CompOp | — |
splitOn 📖 | CompOp | — |
splitOnP 📖 | CompOp | 3 mathmath: splitOnP_eq_splitOnPTR, String.split_of_valid, String.splitToList_of_valid
|
splitOnPTR 📖 | CompOp | 1 mathmath: splitOnP_eq_splitOnPTR
|
sublists 📖 | CompOp | 1 mathmath: sublists_eq_sublistsFast
|
sublists' 📖 | CompOp | — |
sublistsFast 📖 | CompOp | 1 mathmath: sublists_eq_sublistsFast
|
tails 📖 | CompOp | 1 mathmath: tails_eq_tailsTR
|
tailsTR 📖 | CompOp | 1 mathmath: tails_eq_tailsTR
|
takeD 📖 | CompOp | 5 mathmath: takeD_succ, takeD_nil, takeD_eq_takeDTR, takeD_zero, takeDTR_go_eq
|
takeDTR 📖 | CompOp | 1 mathmath: takeD_eq_takeDTR
|
takeList 📖 | CompOp | 1 mathmath: takeList_eq_takeListTR
|
takeListTR 📖 | CompOp | 1 mathmath: takeList_eq_takeListTR
|
takeWhile₂ 📖 | CompOp | 3 mathmath: String.firstDiffPos_loop_eq, takeWhile₂_eq_takeWhile₂TR, String.firstDiffPos_eq
|
takeWhile₂TR 📖 | CompOp | 1 mathmath: takeWhile₂_eq_takeWhile₂TR
|
toChunks 📖 | CompOp | — |
toChunksAux 📖 | CompOp | — |
transpose 📖 | CompOp | — |
traverse 📖 | CompOp | — |
union 📖 | CompOp | — |
zipLeft 📖 | CompOp | — |
zipLeft' 📖 | CompOp | — |
zipRight 📖 | CompOp | — |
zipRight' 📖 | CompOp | — |
zipWithLeft 📖 | CompOp | 1 mathmath: zipWithLeft_eq_zipWithLeftTR
|
zipWithLeft' 📖 | CompOp | 1 mathmath: zipWithLeft'_eq_zipWithLeft'TR
|
zipWithLeft'TR 📖 | CompOp | 1 mathmath: zipWithLeft'_eq_zipWithLeft'TR
|
zipWithLeftTR 📖 | CompOp | 1 mathmath: zipWithLeft_eq_zipWithLeftTR
|
zipWithRight 📖 | CompOp | — |
zipWithRight' 📖 | CompOp | — |
zipWith₃ 📖 | CompOp | — |
zipWith₄ 📖 | CompOp | — |
zipWith₅ 📖 | CompOp | — |
«term_<+~_» 📖 | CompOp | — |