| 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, scanl, scanlM, scanr, scanrM, 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_<+~_» | 129 |
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 | 156 |
| Name | Category | Theorems |
|---|
Chain 📖 | MathDef | 1 mathmath: Chain.nil
|
Chain' 📖 | MathDef | — |
Disjoint 📖 | MathDef | 13 mathmath: disjoint_iff_ne, disjoint_left, disjoint_take_drop, disjoint_comm, singleton_disjoint, disjoint_singleton, disjoint_append_right, disjoint_nil_right, disjoint_right, disjoint_append_left, disjoint_cons_right, disjoint_cons_left, disjoint_nil_left
|
Forall₂ 📖 | CompData | 1 math, 1 bridgemath: forall₂_cons
bridge: all₂_eq_true
|
IsChain 📖 | CompData | 12 mathmath: isChain_idxsOf, isChain_lt_range', chain_lt_range', isChain_cons_cons, isChain_range', isChain_findIdxs, chain_cons, isChain_iff_getElem, Pairwise.isChain, chain_succ_range', Pairwise.chain, isChain_iff_pairwise
|
Subperm 📖 | MathDef | 18 math, 1 bridgemath: subperm_append_left, subperm_of_subset, erase_subperm, singleton_subperm_iff, erase_cons_subperm_cons_erase, subperm_nil, 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_cons_diff, subperm_ext_iff
bridge: isSubperm_iff
|
after 📖 | CompOp | — |
allSome 📖 | CompOp | — |
all₂ 📖 | CompOp | 1 bridgebridge: all₂_eq_true
|
bagInter 📖 | CompOp | — |
countBefore 📖 | CompOp | 22 mathmath: countBefore_zero, snd_idxToSigmaCount, countBefore_nil, Perm.countBefore_idxOfNth, 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, Sublist.coe_idxOrderInj, Subperm.countBefore_idxOfNth, countBefore_eq_count_take, countBefore_lt_count_getElem, countBefore_cons_succ_of_not_beq, coe_idxInj, countBefore_of_ge_length, Sublist.countBefore_idxOfNth, 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 | 27 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
|
findIdxs 📖 | CompOp | 23 mathmath: findIdxs_eq_nil_iff, mem_findIdxs_iff_getElem_sub_pos, findIdx_mem_findIdxs, mem_findIdxs_iff_pos_getElem, findIdx_add_mem_findIdxs, idxsOf_map, unzip_findIdxsValues, pairwise_findIdxs, findIdxs_map, findIdxs_take, isChain_findIdxs, findIdxs_start, getElem_filter_eq_getElem_getElem_findIdxs_sub, findIdxsValues_eq_zip_filter_findIdxs, mem_findIdxs_iff_exists_getElem_pos, findIdxs_nil, length_findIdxs, getElem_filter_eq_getElem_getElem_findIdxs, findIdxs_eq_filterMap_zipIdx, findIdxs_cons, nodup_findIdxs, findIdxs_singleton, findIdxs_append
|
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 | 34 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, Perm.countBefore_idxOfNth, idxOfNth_eq_idxOfNth_iff_of_left_lt_count, idxOfNth_eq_length_iff, 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, Sublist.coe_idxOrderInj, Subperm.countBefore_idxOfNth, idxOfNth_cons, idxOfNth_lt_idxOfNth_iff, coe_idxInj, Sublist.countBefore_idxOfNth, idxOfNth_cons_of_not_beq, idxOfNth_le_length, coe_sigmaCountToIdx, idxOfNth_nil
|
idxsOf 📖 | CompOp | 18 mathmath: isChain_idxsOf, idxsOf_map, pairwise_idxsOf, nodup_idxsOf, mem_idxsOf_iff_getElem_sub_pos, mem_idxsOf_getElem, length_idxsOf, idxsOf_take, idxsOf_append, idxsOf_nil, idxOf_mem_idxsOf, idxsOf_start, mem_idxsOf_iff_exists_getElem_pos, idxOf_add_mem_idxsOf, idxsOf_eq_nil_iff, idxsOf_eq_filterMap_zipIdx, idxsOf_cons, mem_idxsOf_iff_getElem_pos
|
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 | 6 mathmath: partialProds_append, partialProds_cons, partialProds_nil, getElem?_partialProds, take_partialProds, length_partialProds
|
partialSums 📖 | CompOp | 9 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₂
|
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 | 3 mathmath: scanAuxM_cons, scanAuxM_nil, scanAuxM.go_eq_append_map
|
scanl 📖 | CompOp | 25 mathmath: getElem?_succ_scanl, getElem_scanl_zero, length_scanl, scanl_cons, scanl_append, tail_scanl, scanl_reverse, scanl_eq_scanr_reverse, scanl_singleton, scanl_nil, Array.toList_scanl, head_scanl, getLast?_scanl, toArray_scanl, scanlM_pure, getLast_scanl, scanl_map, idRun_scanlM, getElem?_scanl_zero, take_scanl, scanr_reverse, getElem?_scanl, scanr_eq_scanl_reverse, Array.scanl_eq_scanl_toList, scanl_eq_singleton_iff
|
scanlM 📖 | CompOp | 13 mathmath: scanlM_eq_scanrM_reverse, Array.scanlM_eq_scanlM_toList, scanrM_eq_scanlM_reverse, scanrM_reverse, scanlM_nil, toArray_scanlM, Array.scanlM.loop_toList, scanlM_pure, scanlM_reverse, scanlM_map, idRun_scanlM, Array.toList_scanlM, scanlM_cons
|
scanr 📖 | CompOp | 25 mathmath: getLast_scanr, scanr_append, scanr_nil, scanr_singleton, scanr_map, scanl_reverse, idRun_scanrM, drop_scanr, scanl_eq_scanr_reverse, getElem?_scanr, scanr_iff_nil, scanrM_pure, head_scanr, getElem_scanr_zero, getLast?_scanr, getElem?_scanr_zero, scanr_reverse, scanr_cons, Array.scanr_eq_scanr_toList, toArray_scanr, scanr_eq_scanl_reverse, tail_scanr, getElem?_scanr_of_lt, Array.toList_scanr, length_scanr
|
scanrM 📖 | CompOp | 13 mathmath: scanlM_eq_scanrM_reverse, scanrM_concat, idRun_scanrM, Array.scanrM_eq_scanrM_toList, scanrM_eq_scanlM_reverse, scanrM_pure, scanrM_reverse, Array.scanrM.loop_toList, scanrM_nil, scanlM_reverse, Array.toList_scanrM, toArray_scanrM, scanrM_map
|
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 | — |