| Metric | Count |
|---|
| Definitions | 0 |
Theoremsimp, imp', cons_of_imp, cons_of_imp_of_cons, cons_of_imp_of_imp, getElem, imp, of_cons, pairwise, rel, idxOf_getElem, chain, isChain, diff_right, erase_diff_erase_sublist, append_eq_of_isPrefixOf?_eq_some, append_eq_of_isSuffixOf?_eq_some, beq_iff_exists_findIdxNth, chain_cons, chain_lt_range', chain_of_chain_cons, chain_succ_range', cons_diff, cons_diff_of_mem, cons_diff_of_not_mem, cons_union, countBefore_cons, countBefore_cons_succ, countBefore_cons_succ_of_beq, countBefore_cons_succ_of_not_beq, countBefore_eq_count_take, countBefore_idxOfNth_of_lt_count, countBefore_le_count, countBefore_lt_count_getElem, countBefore_lt_count_of_lt_length_of_beq, countBefore_nil, countBefore_of_ge_length, countBefore_zero, countPBefore_cons, countPBefore_cons_succ, countPBefore_cons_succ_of_neg, countPBefore_cons_succ_of_pos, countPBefore_cons_zero, countPBefore_eq_countP_take, countPBefore_findIdxNth_of_lt_countP, countPBefore_le_countP, countPBefore_length, countPBefore_lt_countP_of_lt_length_of_pos, countPBefore_mono, countPBefore_nil, countPBefore_of_ge_length, countPBefore_succ, countPBefore_zero, count_getElem_take_lt_count, count_getElem_take_succ, diff_append, diff_cons, diff_cons_right, diff_eq_foldl, diff_erase, diff_nil, diff_sublist, diff_subset, disjoint_append_left, disjoint_append_right, disjoint_comm, disjoint_cons_left, disjoint_cons_right, disjoint_iff_ne, disjoint_left, disjoint_nil_left, disjoint_nil_right, disjoint_of_disjoint_append_left_left, disjoint_of_disjoint_append_left_right, disjoint_of_disjoint_append_right_left, disjoint_of_disjoint_append_right_right, disjoint_of_disjoint_cons_left, disjoint_of_disjoint_cons_right, disjoint_of_subset_left, disjoint_of_subset_right, disjoint_right, disjoint_singleton, disjoint_symm, disjoint_take_drop, dropInfix?_eq_some_iff, dropInfix?_go_eq_some_iff, dropInfix?_nil, dropLast_eq_eraseIdx, dropPrefix?_append_of_beq, dropPrefix?_eq_some_iff, dropPrefix?_nil, dropSuffix?_eq_some_iff, dropSuffix?_nil, eraseIdx_idxOf_eq_erase, erase_eq_self_iff_forall_bne, exists_of_replaceF, exists_or_eq_self_of_replaceF, extractP_eq_find?_eraseP, finRange_eq_nil_iff, finRange_eq_pmap_range, findIdxNth_cons, findIdxNth_cons_of_neg, findIdxNth_cons_of_pos, findIdxNth_cons_succ, findIdxNth_cons_succ_of_pos, findIdxNth_cons_zero, findIdxNth_cons_zero_of_pos, findIdxNth_countPBefore_of_lt_length_of_pos, findIdxNth_eq_findIdxNth_iff, findIdxNth_eq_findIdxNth_iff_of_left_lt_countP, findIdxNth_eq_findIdxNth_iff_of_right_lt_countP, findIdxNth_eq_findIdxNth_of_ge_countP_ge_countP, findIdxNth_eq_length_iff, findIdxNth_eq_length_of_ge_countP, findIdxNth_le_findIdxNth_iff, findIdxNth_le_length, findIdxNth_lt_findIdxNth_iff, findIdxNth_lt_findIdxNth_iff_of_lt_countP, findIdxNth_lt_length_iff, findIdxNth_lt_length_of_lt_countP, findIdxNth_mono, findIdxNth_nil, findIdxNth_zero, findIdx_add_mem_findIdxs, findIdx_eq_findIdx?, findIdx_mem_findIdxs, findIdxsValues_eq_zip_filter_findIdxs, findIdxs_append, findIdxs_cons, findIdxs_eq_filterMap_zipIdx, findIdxs_eq_nil_iff, findIdxs_map, findIdxs_nil, findIdxs_singleton, findIdxs_start, findIdxs_take, foldlIdx_cons, foldlIdx_const, foldlIdx_eq_foldl_zipIdx, foldlIdx_nil, foldlIdx_start, foldrIdx_cons, foldrIdx_const, foldrIdx_eq_foldr_zipIdx, foldrIdx_nil, foldrIdx_start, foldr_eq_foldl, forIn_eq_bindList, ge_of_mem_findIdxs, ge_of_mem_idxsOf, get?_set_of_lt, get?_set_of_lt', getElem?_set_eq_of_lt, getElem?_set_of_lt, getElem?_set_of_lt', getElem_filter_eq_getElem_getElem_findIdxs, getElem_filter_eq_getElem_getElem_findIdxs_sub, getElem_findIdxs_eq_findIdxNth, getElem_findIdxs_eq_findIdxNth_add, getElem_findIdxs_lt, getElem_getElem_findIdxs, getElem_getElem_findIdxs_sub, getElem_getElem_idxsOf, getElem_getElem_idxsOf_of_lawful, getElem_getElem_idxsOf_sub, getElem_getElem_idxsOf_sub_of_lawful, getElem_idxOf, getElem_idxOfNth_beq, getElem_idxOfNth_eq, getElem_idxOf_eq_idxOfNth, getElem_idxOf_eq_idxOfNth_add, getElem_idxsOf_lt, getElem_mk, getElem_zero_findIdxs_eq_findIdx, getElem_zero_findIdxs_eq_findIdx_add, getElem_zero_idxsOf_eq_idxOf, getElem_zero_idxsOf_eq_idxOf_add, get_finRange, idxOfNth_cons, idxOfNth_cons_of_beq, idxOfNth_cons_of_not_beq, idxOfNth_cons_succ, idxOfNth_cons_succ_of_beq, idxOfNth_cons_zero, idxOfNth_cons_zero_of_beq, idxOfNth_countBefore_getElem, idxOfNth_countBefore_of_lt_length_of_beq, idxOfNth_eq_idxOfNth_iff, idxOfNth_eq_idxOfNth_iff_of_left_lt_count, idxOfNth_eq_idxOfNth_iff_of_right_lt_count, idxOfNth_eq_idxOfNth_of_ge_countP_ge_countP, idxOfNth_eq_length_iff, idxOfNth_eq_length_of_ge_count, idxOfNth_le_length, idxOfNth_lt_idxOfNth_iff, idxOfNth_lt_idxOfNth_iff_of_lt_count, idxOfNth_lt_length_iff, idxOfNth_lt_length_of_lt_count, idxOfNth_mono, idxOfNth_nil, idxOfNth_zero, idxOf_add_mem_idxsOf, idxOf_eq_getD_idxOf?, idxOf_eq_idxOf?, idxOf_mem_idxsOf, idxsOf_append, idxsOf_cons, idxsOf_eq_filterMap_zipIdx, idxsOf_eq_nil_iff, idxsOf_map, idxsOf_nil, idxsOf_start, idxsOf_take, insertP_cons_neg, insertP_cons_pos, insertP_loop, insertP_nil, instNeZeroNatLengthCons, inter_def, isChain_cons_of_isChain_cons_cons, isChain_findIdxs, isChain_idxsOf, isChain_iff_getElem, isChain_iff_pairwise, isChain_lt_range', isChain_of_isChain_cons, isChain_of_isChain_cons_cons, isChain_range', isPrefixOf?_eq_some_iff_append_eq, isSome_isPrefixOf?_eq_isPrefixOf, isSome_isSuffixOf?_eq_isSuffixOf, isSuffixOf?_eq_some_iff_append_eq, le_getElem_findIdxs, le_getElem_idxsOf, length_findIdxs, length_idxsOf, length_insertP, length_replaceF, length_tail_add_one, lt_add_of_mem_findIdxs, lt_add_of_mem_idxsOf, map_coe_finRange_eq_range, map_getElem_finRange, map_get_finRange, mem_diff_of_mem, mem_findIdxs_iff_exists_getElem_pos, mem_findIdxs_iff_getElem_sub_pos, mem_findIdxs_iff_pos_getElem, mem_idxsOf_getElem, mem_idxsOf_iff_exists_getElem_pos, mem_idxsOf_iff_getElem_pos, mem_idxsOf_iff_getElem_sub_pos, mem_insertP, mem_inter_iff, mem_union_iff, modify_eq_set_get, modify_eq_set_get?, modify_eq_set_getElem?, next?_cons, next?_nil, nil_diff, nil_union, nodup_finRange, nodup_findIdxs, nodup_idxsOf, pair_mem_product, pairwise_cons_cons, pairwise_findIdxs, pairwise_idxsOf, pairwise_le_finRange, pairwise_lt_finRange, pos_findIdxNth_getElem, pos_iff_exists_findIdxNth, prod_append, prod_concat, prod_cons, prod_eq_foldl, prod_eq_foldr, prod_flatten, prod_nil, prod_one_cons, prod_pair, prod_singleton, rel_of_chain_cons, rel_of_isChain_cons_cons, replaceF_cons, replaceF_cons_of_none, replaceF_cons_of_some, replaceF_nil, replaceF_of_forall_none, reverse_singleton, set_eq_modify, set_eq_take_cons_drop, singleton_disjoint, sum_append, sum_concat, sum_eq_foldl, sum_eq_foldr, sum_flatten, sum_pair, sum_singleton, sum_zero_cons, take_succ_drop, union_def, unzip_findIdxsValues | 305 |
| Total | 305 |