Def | | [list_to_function] | ||
Def | | [find_first_iter] | ||
Def | | [is_permutation] | ||
Def | | [fin_enum] | ||
Def | | [seq_nil] | ||
Def | | [seq_cons] | ||
Def | | [list_member_type] | ||
Def | | [is_one_one_corr_rel] | ||
Def | | [prop] | core | |
Def | | [ndiff] | int 2 | |
Def | | [isect_two] | LogicSupplement | |
Def | | [is_finite_type] | ||
Def | | [unboundedly_infinite] | ||
Def | | [productively_infinite] | ||
Def | | [sized_mset] | ||
Def | | [int_upper] | int 1 | |
Def | | [sized_bool] | ||
Def | | [nat] | int 1 | |
Def | | [int_seg] | int 1 | |
Def | | [int_iseg] | int 1 | |
Def | | [lelt] | int 1 | |
Def | | [le] | core | |
Def | | [eqfun_p] | rel 1 | |
Def | | [is_discrete] | LogicSupplement | |
Def | | [decidable] | core | |
Def | | [singleton] | core | |
Def | | [exteq] | LogicSupplement | |
Def | | [bijection_type] | ||
Def | | [inhabited_uniquely] | LogicSupplement | |
Def | | [subtype] | core | |
Def | | [nat_plus] | int 1 | |
Def | | [surjection_type] | ||
Def | | [cand] | core | |
Def | | [nequal] | core | |
Def | | [rel_1_1_b] | ||
Def | | [rel_1_1] | ||
Def | | [sq_stable] | core | |
Def | | [least] | ||
Def | | [assert] | bool 1 | |
Def | | [infix_ap] | core | |
Def | | [equiv_rel_sep] | LogicSupplement | |
Def | | [equiv_rel] | rel 1 | |
Def | | [trans] | rel 1 | |
Def | | [squash] | core | |
Def | | [one_one_corr_fams] | ||
Def | | [union_to_sigma] | ||
Def | | [sigma_to_union] | ||
Def | | [factorial_via_iter] | IteratedBinops | |
Def | | [Dedekind_infinite] | ||
Def | | [fun_over_st] | LogicSupplement | |
Def | | [guard] | core | |
Def | | [quotient_sep] | LogicSupplement | |
Def | | [allst] | LogicSupplement | |
Def | | [unit] | core | |
Def | | [factorial_tail_via_iter] | IteratedBinops | |
Def | | [prev_nat_pair] | ||
Def | | [nat_to_nat_pair] | ||
Def | | [same_range_sep] | ||
Def | | [exists_unique] | LogicSupplement | |
Def | | [all] | core | |
Def | | [and] | core | |
Def | | [or] | core | |
Def | | [false] | core | |
Def | | [ycomb] | core | |
Def | | [ifthenelse] | bool 1 | |
Def | | [compose_iter] | ||
Def | | [delete_fenum_value] | ||
Def | | [next_nat_pair] | ||
Def | | [eq_int] | bool 1 | |
Def | | [iff] | core | |
Def | | [implies] | core | |
Def | | [exists] | core | |
Def | | [inv_pair] | ||
Def | | [injection_type] | ||
Def | | [inhabited] | LogicSupplement | |
Def | | [not] | core | |
Def | | [boolsize] | ||
Def | | [msize] | ||
Def | | [iter_via_intseg] | IteratedBinops | |
Def | | [bool] | bool 1 | |
Def | | [is_list_mem] | ||
Def | | [one_one_corr_2] | ||
Def | | [one_one_corr] | ||
Def | | [replace_fn_values] | ||
Def | | [inv_funs] | ||
Def | | [biject] | ||
Def | | [inject] | ||
Def | | [surject] | ||
Def | | [is_one_one_corr] | ||
Def | | [inv_funs_2] | ||
Def | | [select] | ||
Def | | [imax] | int 2 | |
Def | | [sym] | rel 1 | |
Def | | [refl] | rel 1 | |
Def | | [so_lambda2] | ||
Def | | [is_the] | LogicSupplement | |
Def | | [rev_implies] | core | |
Def | | [nth_tl] | ||
Def | | [le_int] | bool 1 | |
Def | | [lt_int] | bool 1 | |
Def | | [tidentity] | ||
Def | | [compose] | ||
Def | | [hd] | ||
Def | | [identity] | ||
Def | | [tl] | ||
Def | | [bnot] | bool 1 |
About: