| Metric | Count |
|---|
DefinitionsDom, assert, bind, equivOption, get, getOrElse, instAdd, instAppend, instCoeOption, instDiv, instInhabited, instInter, instInv, instMembership, instMod, instMonad, instMul, instNeg, instOne, instOrderBot, instPartialOrder, instSDiff, instSub, instUnion, instZero, map, none, noneDecidable, ofOption, ofOptionDecidable, restrict, some, someDecidable, toOption, unwrap | 35 |
Theoremsbind, of_bind, toOption, left_unique, right_unique, add_def, add_get_eq, add_mem_add, append_def, append_get_eq, append_mem_append, assert_defined, assert_neg, assert_pos, bind_assoc, bind_defined, bind_dom, bind_eq_bind, bind_le, bind_map, bind_none, bind_of_mem, bind_some, bind_some_eq_map, bind_some_right, bind_toOption, coe_none, coe_some, div_def, div_get_eq, div_mem_div, dom_iff_mem, elim_toOption, eq_get_iff_mem, eq_iff_of_dom, eq_none_iff, eq_none_iff', eq_none_or_eq_some, eq_of_get_eq_get, eq_of_mem, eq_some_iff, eta, ext, ext', ext_iff, getOrElse_none, getOrElse_of_dom, getOrElse_of_not_dom, getOrElse_some, get_eq_get_of_eq, get_eq_iff_eq_some, get_eq_iff_mem, get_eq_of_mem, get_mem, get_some, induction_on, instLawfulMonad, inter_def, inter_get_eq, inter_mem_inter, inv_def, inv_mem_inv, inv_some, le_total_of_le_of_le, left_dom_of_add_dom, left_dom_of_append_dom, left_dom_of_div_dom, left_dom_of_inter_dom, left_dom_of_mod_dom, left_dom_of_mul_dom, left_dom_of_sdiff_dom, left_dom_of_sub_dom, left_dom_of_union_dom, map_Dom, map_bind, map_eq_map, map_get, map_id', map_map, map_none, map_some, mem_assert, mem_assert_iff, mem_bind, mem_bind_iff, mem_coe, mem_eq, mem_map, mem_map_iff, mem_mk_iff, mem_ofOption, mem_restrict, mem_right_unique, mem_some, mem_some_iff, mem_toOption, mem_unique, mod_def, mod_get_eq, mod_mem_mod, mul_def, mul_get_eq, mul_mem_mul, ne_none_iff, neg_def, neg_mem_neg, neg_some, none_ne_some, none_toOption, notMem_none, not_none_dom, ofOption_dom, ofOption_eq_get, of_toOption, one_def, one_mem_one, pure_eq_some, ret_eq_some, right_dom_of_add_dom, right_dom_of_append_dom, right_dom_of_div_dom, right_dom_of_inter_dom, right_dom_of_mod_dom, right_dom_of_mul_dom, right_dom_of_sdiff_dom, right_dom_of_sub_dom, right_dom_of_union_dom, sdiff_def, sdiff_get_eq, sdiff_mem_sdiff, some_add_some, some_append_some, some_div_some, some_dom, some_get, some_inj, some_injective, some_inter_some, some_mod_some, some_mul_some, some_ne_none, some_sdiff_some, some_sub_some, some_toOption, some_union_some, sub_def, sub_get_eq, sub_mem_sub, subsingleton, toOption_eq_none, toOption_eq_none_iff, toOption_eq_some_iff, toOption_isSome, to_ofOption, union_def, union_get_eq, union_mem_union, zero_def, zero_mem_zero | 159 |
| Total | 194 |
| Name | Category | Theorems |
|---|
Dom π | MathDef | 48 mathmath: partialFunToPointed_map, Finset.pimage_eq_image_filter, Turing.tr_eval_dom, PartENat.dom_one, PartENat.dom_of_le_some, PartENat.dom_of_le_natCast, Partrec.merge', elim_toOption, Nat.rfind_dom, ofOption_dom, eta, Nat.rfindOpt_dom, PartENat.not_dom_iff_eq_top, partialFunEquivPointed_functor_map_toFun, PFun.dom_prodLift, eq_none_iff', toOption_eq_none, toOption_eq_none_iff, PartENat.toWithTop_add, ComputablePred.halting_problem_not_re, PartENat.ne_top_iff_dom, dom_iff_mem, PartENat.instCanLiftNatCastDom, PartENat.dom_some, PartENat.dom_natCast, not_none_dom, PFun.prodMap_apply, ComputablePred.halting_problem, PartENat.dom_ofNat, PartENat.dom_zero, PartENat.withTopEquiv_apply, PFun.dom_prodMap, PartENat.dom_of_lt, Nat.rfind_dom', Nat.Partrec.merge', Partrec.dom_re, toOption_isSome, ComputablePred.halting_problem_re, bind_dom, partialFunEquivPointed_inverse_map_Dom, Turing.TM2to1.tr_eval_dom, PFun.prodLift_apply, PartENat.find_dom, some_dom, PFun.dom_toSubtype_apply_iff, mem_eq, PFun.dom_of_mem_fix, map_Dom
|
assert π | CompOp | 5 mathmath: assert_neg, assert_defined, assert_pos, mem_assert, mem_assert_iff
|
bind π | CompOp | 48 mathmath: mem_bind_iff, PFun.bind_apply, Partrec.rfindOpt, map_bind, Nat.Partrec.prec', Nat.Partrec'.to_part, bind_some, bind_some_right, Partrec.sumCasesOn_right, Dom.bind, Nat.Partrec.Code.computable_recOn, OmegaCompletePartialOrder.ContinuousHom.bind_apply, Partrec.some, bind_defined, bind_toOption, Nat.Partrec.Code.eval_pappAck_step_succ, bind_of_mem, Partrecβ.comp, Computable.ofOption, Partrec.nat_iff, bind_some_eq_map, Computable.partrec, Partrec.nat_casesOn_right, Nat.Partrec'.part_iff, Partrec.const', Nat.Partrec'.bind, bind_map, bind_none, Partrec.sumCasesOn_left, Partrec.none, bind_assoc, Monotone.partBind, Partrec.bind_decodeβ_iff, Partrec.option_some_iff, Decidable.Partrec.const', mem_bind, Partrec.map_encode_iff, Partrec.optionCasesOn_right, bind_dom, Partrecβ.unpaired, Partrec.rfind, PFun.comp_apply, bind_eq_bind, PFun.Part.bind_comp, Antitone.partBind, Nat.Partrec'.part_iffβ, OrderHom.partBind_coe, Partrec.sumCasesOn
|
equivOption π | CompOp | β |
get π | CompOp | 52 mathmath: Finset.pimage_eq_image_filter, sub_get_eq, elim_toOption, PartENat.get_one, PartENat.eq_natCast_sub_of_add_eq_natCast, get_eq_of_mem, get_eq_iff_eq_some, mul_get_eq, PartENat.lt_coe_iff, eta, PartENat.get_natCast, inter_get_eq, mod_get_eq, Dom.bind, PartENat.le_coe_iff, eq_iff_of_dom, get_eq_get_of_eq, PartENat.get_eq_iff_eq_some, PartENat.get_le_get, PFun.fn_apply, PartENat.lt_def, map_get, get_mem, eq_get_iff_mem, PartENat.find_get, PartENat.natCast_get, PFun.get_prodLift, union_get_eq, getOrElse_of_dom, PartENat.le_def, PartENat.coe_lt_iff, PartENat.get_eq_iff_eq_coe, PFun.prodMap_apply, get_eq_iff_mem, PFun.get_prodMap, PartENat.get_zero, some_get, append_get_eq, Dom.toOption, PartENat.coe_le_iff, PartENat.get_ofNat', bind_dom, sdiff_get_eq, partialFunEquivPointed_inverse_map_get_coe, add_get_eq, PartENat.get_natCast', PFun.prodLift_apply, div_get_eq, get_some, mem_eq, PartENat.coe_add_get, PartENat.get_add
|
getOrElse π | CompOp | 4 mathmath: getOrElse_of_dom, getOrElse_of_not_dom, getOrElse_some, getOrElse_none
|
instAdd π | CompOp | 3 mathmath: add_def, some_add_some, add_mem_add
|
instAppend π | CompOp | 3 mathmath: append_mem_append, append_def, some_append_some
|
instCoeOption π | CompOp | β |
instDiv π | CompOp | 3 mathmath: div_def, some_div_some, div_mem_div
|
instInhabited π | CompOp | β |
instInter π | CompOp | 3 mathmath: inter_def, some_inter_some, inter_mem_inter
|
instInv π | CompOp | 3 mathmath: inv_mem_inv, inv_def, inv_some
|
instMembership π | CompOp | 55 mathmath: mem_bind_iff, Partrec.merge', one_mem_one, mem_mk_iff, mem_ofOption, Nat.rfind_dom, eq_some_iff, Nat.rfind_min', mem_some_iff, PFun.mem_dom, Mem.right_unique, PFun.image_def, coe_toFinset, ext_iff, Nat.mem_rfind, mem_toOption, PFun.mem_res, Turing.mem_eval, PFun.mem_restrict, get_mem, Finset.mem_pimage, mem_restrict, eq_get_iff_mem, Partrec.merge, mem_coe, subsingleton, dom_iff_mem, mem_ΟSup, mem_some, eq_none_iff, Nat.rfindOpt_mono, PFun.mem_toSubtype_iff, Mem.left_unique, get_eq_iff_mem, Partrec.fix_aux, toOption_eq_some_iff, Nat.rfind_dom', PFun.mem_prodMap, Nat.Partrec.merge', PFun.mem_image, zero_mem_zero, notMem_none, PFun.mem_fix_iff, Fix.mem_iff, mem_map_iff, Nat.Partrec.Code.evaln_sound, Nat.Partrec.Code.evaln_complete, PFun.mem_prodLift, mem_toFinset, mem_eq, PFun.dom_eq, PFun.ext_iff, mem_assert_iff, PFun.Preimage_def, PFun.mem_preimage
|
instMod π | CompOp | 3 mathmath: mod_mem_mod, mod_def, some_mod_some
|
instMonad π | CompOp | 44 mathmath: inter_def, append_def, Turing.ToPartrec.Code.comp_eval, add_def, Turing.ToPartrec.Code.nil_eval, Turing.tr_eval', Nat.Partrec.prec', Turing.ToPartrec.Code.pred_eval, Turing.ToPartrec.Code.head_eval, Turing.ToPartrec.stepNormal_eval, bind_le, Turing.ToPartrec.Cont.then_eval, Turing.ToPartrec.Code.zero'_eval, Turing.ToPartrec.Code.tail_eval, Turing.ToPartrec.Code.id_eval, OmegaCompletePartialOrder.ContinuousHom.seq_apply, div_def, map_eq_map, Nat.Partrec.rfind', Nat.Partrec.Code.eval_prec_succ, OmegaCompletePartialOrder.ContinuousHom.ΟScottContinuous.seq, Vector.mOfFn_part_some, Turing.ToPartrec.Code.cons_eval, Turing.ToPartrec.stepRet_eval, Turing.ToPartrec.cont_eval_fix, Antitone.partSeq, sub_def, instLawfulMonad, ret_eq_some, Monotone.partSeq, Turing.ToPartrec.Code.exists_code, mod_def, OmegaCompletePartialOrder.ContinuousHom.ΟSup_bind, Turing.ToPartrec.Code.succ_eval, Turing.PartrecToTM2.tr_eval, Turing.ToPartrec.Code.Ok.zero, sdiff_def, union_def, mul_def, OmegaCompletePartialOrder.ContinuousHom.ΟScottContinuous.map, Turing.ToPartrec.Code.zero_eval, pure_eq_some, bind_eq_bind, OmegaCompletePartialOrder.ContinuousHom.ΟScottContinuous.bind
|
instMul π | CompOp | 3 mathmath: mul_mem_mul, some_mul_some, mul_def
|
instNeg π | CompOp | 3 mathmath: neg_some, neg_mem_neg, neg_def
|
instOne π | CompOp | 2 mathmath: one_mem_one, one_def
|
instOrderBot π | CompOp | β |
instPartialOrder π | CompOp | 14 mathmath: Fix.exists_fix_le_approx, toUnitMono_coe, Fix.approx_mem_approxChain, Fix.approx_le_fix, bind_le, mem_ΟSup, fix_eq_ΟSup, mem_chain_of_mem_ΟSup, ΟScottContinuous_toUnitMono, Fix.approx_mono', Fix.mem_iff, fix_eq_ΟSup_of_ΟScottContinuous, OrderHom.partBind_coe, Fix.approx_mono
|
instSDiff π | CompOp | 3 mathmath: some_sdiff_some, sdiff_def, sdiff_mem_sdiff
|
instSub π | CompOp | 3 mathmath: sub_mem_sub, some_sub_some, sub_def
|
instUnion π | CompOp | 3 mathmath: union_mem_union, some_union_some, union_def
|
instZero π | CompOp | 2 mathmath: zero_def, zero_mem_zero
|
map π | CompOp | 52 mathmath: inter_def, append_def, add_def, Partrec.rfindOpt, map_bind, Nat.Partrec'.to_part, Partrec.sumCasesOn_right, Nat.Partrec'.map, Nat.Partrec.Code.computable_recOn, Monotone.partMap, div_def, Partrec.some, map_get, map_eq_map, Nat.Partrec.rfind', Partrecβ.comp, Computable.ofOption, Partrec.nat_iff, map_map, inv_def, Antitone.partMap, bind_some_eq_map, Computable.partrec, Partrec.nat_casesOn_right, Nat.Partrec'.part_iff, Partrec.const', sub_def, map_id', bind_map, Partrec.sumCasesOn_left, mod_def, map_some, Partrec.none, Partrec.bind_decodeβ_iff, Partrec.option_some_iff, Decidable.Partrec.const', sdiff_def, union_def, mul_def, Partrec.map_encode_iff, Partrec.optionCasesOn_right, Turing.ToPartrec.Code.fix_eval, Partrecβ.unpaired, mem_map, neg_def, mem_map_iff, map_none, Partrec.rfind, Nat.Partrec'.part_iffβ, map_Dom, OmegaCompletePartialOrder.ContinuousHom.map_apply, Partrec.sumCasesOn
|
none π | CompOp | 16 mathmath: Nat.Partrec.none, PartENat.top_eq_none, assert_neg, eq_none_iff', ΟSup_eq_none, eq_none_iff, toFinset_none, none_toOption, not_none_dom, fix_def', bind_none, getOrElse_none, coe_none, notMem_none, map_none, eq_none_or_eq_some
|
noneDecidable π | CompOp | 1 mathmath: PartENat.toWithTop_top
|
ofOption π | CompOp | 34 mathmath: Nat.Partrec.ppred, ofOption_eq_get, mem_ofOption, Partrec.rfindOpt, ofOption_dom, Nat.Partrec'.to_part, PartialFun.Iso.mk_inv, Partrec.sumCasesOn_right, coe_some, Nat.Partrec.Code.computable_recOn, Partrec.some, mem_coe, Partrecβ.comp, Computable.ofOption, Partrec.nat_iff, Computable.partrec, Partrec.nat_casesOn_right, Nat.Partrec'.part_iff, Partrec.const', Partrec.sumCasesOn_left, Partrec.none, Partrec.bind_decodeβ_iff, Partrec.option_some_iff, Decidable.Partrec.const', coe_none, Partrec.map_encode_iff, Partrec.optionCasesOn_right, Partrecβ.unpaired, of_toOption, Partrec.rfind, PartialFun.Iso.mk_hom, Nat.Partrec'.part_iffβ, Partrec.sumCasesOn, to_ofOption
|
ofOptionDecidable π | CompOp | 1 mathmath: to_ofOption
|
restrict π | CompOp | 1 mathmath: mem_restrict
|
some π | CompOp | 44 mathmath: neg_some, one_def, some_injective, Nat.Partrec.Code.eval_const, some_toOption, get_eq_iff_eq_some, eq_some_iff, bind_some, bind_some_right, mem_some_iff, coe_some, PFun.coe_val, some_add_some, some_inter_some, toFinset_some, some_union_some, PFun.id_apply, Partrec.some, some_inj, some_sdiff_some, ne_none_iff, mem_ΟSup, Vector.mOfFn_part_some, Nat.Partrec.Code.eval_id, mem_some, inv_some, bind_some_eq_map, some_sub_some, mem_chain_of_mem_ΟSup, ret_eq_some, getOrElse_some, Finset.pimage_some, map_some, some_get, zero_def, some_mul_some, some_append_some, some_mod_some, some_div_some, Nat.Partrec.some, pure_eq_some, some_dom, eq_none_or_eq_some, Nat.Partrec.Code.eval_pappAck
|
someDecidable π | CompOp | 2 mathmath: PartENat.toWithTop_one, PartENat.toWithTop_zero
|
toOption π | CompOp | 14 mathmath: partialFunToPointed_map, elim_toOption, some_toOption, mem_toOption, partialFunEquivPointed_functor_map_toFun, toOption_eq_none, toOption_eq_none_iff, bind_toOption, none_toOption, toOption_eq_some_iff, Dom.toOption, toOption_isSome, of_toOption, to_ofOption
|
unwrap π | CompOp | β |