bend-mathlib

bend-mathlib/algebra.bend: abstract associativity/commutativity theorems and their Nat/Bool/List instances.

Owner: MuhDur

Versions

Changes between versions

• 0.1.0.0 → 0.1.0.1: no API changes
• 0.1.0.1 → 0.2.0.0: added: bool.bend/and_not_self, bool.bend/and_not_self_sym, bool.bend/and_or_absorb, bool.bend/and_or_absorb_sym, bool.bend/and_or_distrib_left, bool.bend/and_or_distrib_left_sym, bool.bend/and_self, bool.bend/and_self_sym, bool.bend/eq_true_of_ne_false, bool.bend/not_inj, bool.bend/or_and_absorb, bool.bend/or_and_absorb_sym, bool.bend/or_and_distrib_left, bool.bend/or_and_distrib_left_sym, bool.bend/or_not_self, bool.bend/or_not_self_sym, bool.bend/or_self, bool.bend/or_self_sym, bool.bend/xor_assoc, bool.bend/xor_assoc_sym, bool.bend/xor_comm, bool.bend/xor_comm_sym, bool.bend/xor_false, bool.bend/xor_false_sym, bool.bend/xor_self, bool.bend/xor_self_sym, bool.bend/xor_true, bool.bend/xor_true_sym, list.bend/all_append, list.bend/all_append_sym, list.bend/any_append, list.bend/any_append_sym, list.bend/append_cons, list.bend/append_cons_sym, list.bend/concat_append, list.bend/concat_append_sym, list.bend/contains_append, list.bend/contains_append_sym, list.bend/drop_drop, list.bend/drop_drop_sym, list.bend/drop_length, list.bend/drop_length_sym, list.bend/drop_nil, list.bend/drop_nil_sym, list.bend/drop_zero, list.bend/drop_zero_sym, list.bend/filter_append, list.bend/filter_append_sym, list.bend/foldl_append, list.bend/foldl_append_sym, list.bend/internal_filter_put_append, list.bend/internal_length_filter_put_le, list.bend/internal_length_range_go, list.bend/internal_map_reverse_go, list.bend/length_cons, list.bend/length_cons_sym, list.bend/length_drop, list.bend/length_drop_sym, list.bend/length_filter_le, list.bend/length_filter_le_sym, list.bend/length_nil, list.bend/length_nil_sym, list.bend/length_range, list.bend/length_range_sym, list.bend/length_replicate, list.bend/length_replicate_sym, list.bend/length_take, list.bend/length_take_sym, list.bend/length_zip, list.bend/length_zip_sym, list.bend/map_reverse, list.bend/map_reverse_sym, list.bend/reverse_nil, list.bend/reverse_nil_sym, list.bend/reverse_singleton, list.bend/reverse_singleton_sym, list.bend/take_length, list.bend/take_length_sym, list.bend/take_nil, list.bend/take_nil_sym, list.bend/take_take, list.bend/take_take_sym, list.bend/take_zero, list.bend/take_zero_sym, nat.bend/add_le_add_left, nat.bend/add_sub_cancel, nat.bend/add_sub_cancel_left, nat.bend/add_sub_cancel_left_sym, nat.bend/add_sub_cancel_sym, nat.bend/double_eq_add, nat.bend/double_eq_add_sym, nat.bend/eq_of_is_eq, nat.bend/is_eq_comm, nat.bend/is_eq_comm_sym, nat.bend/is_eq_refl, nat.bend/is_eq_refl_sym, nat.bend/is_ge_eq_is_le, nat.bend/is_ge_eq_is_le_sym, nat.bend/is_gt_eq_is_lt, nat.bend/is_gt_eq_is_lt_sym, nat.bend/is_lt_eq_succ_le, nat.bend/is_lt_eq_succ_le_sym, nat.bend/le_max_left, nat.bend/le_max_right, nat.bend/le_of_succ_le_succ, nat.bend/le_zero_eq, nat.bend/lt_of_le_of_lt, nat.bend/lt_of_lt_of_le, nat.bend/lt_succ_self, nat.bend/lt_zero, nat.bend/max_assoc, nat.bend/max_assoc_sym, nat.bend/max_comm, nat.bend/max_comm_sym, nat.bend/max_self, nat.bend/max_self_sym, nat.bend/max_zero, nat.bend/max_zero_sym, nat.bend/min_add_max, nat.bend/min_add_max_sym, nat.bend/min_assoc, nat.bend/min_assoc_sym, nat.bend/min_comm, nat.bend/min_comm_sym, nat.bend/min_le_left, nat.bend/min_le_right, nat.bend/min_self, nat.bend/min_self_sym, nat.bend/min_zero, nat.bend/min_zero_sym, nat.bend/not_is_le, nat.bend/not_is_le_sym, nat.bend/not_is_lt, nat.bend/not_is_lt_sym, nat.bend/one_pow, nat.bend/one_pow_sym, nat.bend/pow_add, nat.bend/pow_add_sym, nat.bend/pow_one, nat.bend/pow_one_sym, nat.bend/pow_succ, nat.bend/pow_succ_sym, nat.bend/pow_zero, nat.bend/pow_zero_sym, nat.bend/sub_add_cancel, nat.bend/sub_le, nat.bend/sub_self, nat.bend/sub_self_sym, nat.bend/sub_sub, nat.bend/sub_sub_sym, nat.bend/sub_zero, nat.bend/sub_zero_sym, nat.bend/succ_le_succ, nat.bend/succ_sub_succ, nat.bend/succ_sub_succ_sym, nat.bend/zero_max, nat.bend/zero_max_sym, nat.bend/zero_min, nat.bend/zero_min_sym, nat.bend/zero_sub, nat.bend/zero_sub_sym
• 0.2.0.0 → 0.3.0.0: added: list.bend/internal_and_left, list.bend/internal_and_right, list.bend/internal_mem_append_left, list.bend/internal_mem_append_right, list.bend/internal_or_of_or, list.bend/internal_or_of_right, list.bend/mem, list.bend/mem_append_left, list.bend/mem_append_right, list.bend/mem_cons_of_mem, list.bend/mem_cons_self, list.bend/not_mem_nil, list.bend/sorted_by, list.bend/sorted_cons_cons_elim_le, list.bend/sorted_cons_cons_elim_tail, list.bend/sorted_cons_cons_intro, list.bend/sorted_nil, list.bend/sorted_single, list.bend/sorted_tail, perm.bend/evens, perm.bend/insert_by, perm.bend/insert_by_perm, perm.bend/internal_append_nil, perm.bend/internal_apply_app, perm.bend/internal_apply_invert, perm.bend/internal_apply_length, perm.bend/internal_apply_shift, perm.bend/internal_cons_eq, perm.bend/internal_ins_pick, perm.bend/internal_invert, perm.bend/internal_length_eq, perm.bend/internal_merge_pick, perm.bend/internal_perm_dup_nat, perm.bend/internal_perm_length_nat, perm.bend/internal_perm_nil_nat, perm.bend/internal_perm_sym_nat, perm.bend/internal_shift, perm.bend/internal_sort_nat_test, perm.bend/internal_swap_at_invol, perm.bend/internal_swap_at_length, perm.bend/internal_swap_head_invol, perm.bend/internal_swap_head_length, perm.bend/internal_sym_eq, perm.bend/internal_trans_eq, perm.bend/isort_by, perm.bend/isort_by_perm, perm.bend/isort_by_perm_nat, perm.bend/merge_by, perm.bend/merge_by_perm, perm.bend/merge_by_perm_nat, perm.bend/msort_by, perm.bend/msort_by_perm, perm.bend/odds, perm.bend/perm_append, perm.bend/perm_append_comm, perm.bend/perm_append_nil, perm.bend/perm_append_right, perm.bend/perm_cons, perm.bend/perm_dup, perm.bend/perm_length, perm.bend/perm_move, perm.bend/perm_move_rev, perm.bend/perm_nil, perm.bend/perm_refl, perm.bend/perm_swap, perm.bend/perm_sym, perm.bend/perm_trans, perm.bend/sort_by, perm.bend/sort_by_perm, perm.bend/sort_by_perm_nat, perm.bend/split_perm, sort.bend/insert_by_sorted, sort.bend/internal_cons_ins_step, sort.bend/internal_insert_step, sort.bend/internal_le_flip_nat, sort.bend/internal_sorted_cons_cons_elim_le, sort.bend/internal_sorted_cons_cons_elim_tail, sort.bend/internal_sorted_cons_cons_intro, sort.bend/internal_sorted_cons_ins, sort.bend/internal_sorted_single, sort.bend/internal_sorted_tail, sort.bend/isort_by_sorted, sort.bend/isort_by_sorted_nat
• 0.3.0.0 → 0.4.0.0: added: algebra.bend/bool_and_left_comm, algebra.bend/bool_and_left_comm_sym, algebra.bend/bool_and_right_comm, algebra.bend/bool_and_right_comm_sym, algebra.bend/bool_or_left_comm, algebra.bend/bool_or_left_comm_sym, algebra.bend/bool_or_right_comm, algebra.bend/bool_or_right_comm_sym, algebra.bend/foldl_op_eq_foldr_op, algebra.bend/foldl_op_eq_foldr_op_sym, algebra.bend/internal_bool_and_assoc, algebra.bend/internal_bool_and_comm, algebra.bend/internal_bool_or_assoc, algebra.bend/internal_bool_or_comm, algebra.bend/internal_foldl_foldr, algebra.bend/internal_list_nat_append_assoc, algebra.bend/internal_nat_add_assoc, algebra.bend/internal_nat_add_comm, algebra.bend/internal_nat_mul, algebra.bend/internal_nat_mul_assoc, algebra.bend/internal_nat_mul_comm, algebra.bend/list_nat_append_assoc4, algebra.bend/list_nat_append_assoc4_sym, algebra.bend/nat_add_four, algebra.bend/nat_add_four_sym, algebra.bend/nat_add_left_comm, algebra.bend/nat_add_left_comm_sym, algebra.bend/nat_add_right_comm, algebra.bend/nat_add_right_comm_sym, algebra.bend/nat_mul_four, algebra.bend/nat_mul_four_sym, algebra.bend/nat_mul_left_comm, algebra.bend/nat_mul_left_comm_sym, algebra.bend/nat_mul_right_comm, algebra.bend/nat_mul_right_comm_sym, algebra.bend/op_assoc4, algebra.bend/op_assoc4_sym, algebra.bend/op_comm3, algebra.bend/op_comm3_sym, algebra.bend/op_four, algebra.bend/op_four_sym, algebra.bend/op_left_comm, algebra.bend/op_left_comm_sym, algebra.bend/op_right_comm, algebra.bend/op_right_comm_sym, bool.bend/cmp_refl, bool.bend/cmp_refl_sym, bool.bend/eq_of_cmp_eq, bool.bend/internal_false_ne_true, maybe.bend/maybe_bind_assoc, maybe.bend/maybe_bind_assoc_sym, maybe.bend/maybe_bind_pure, maybe.bend/maybe_bind_pure_sym, maybe.bend/maybe_map_compose, maybe.bend/maybe_map_compose_sym, maybe.bend/maybe_map_pure, maybe.bend/maybe_map_pure_sym, maybe.bend/maybe_pure_bind, maybe.bend/maybe_pure_bind_sym, nat.bend/add_div_left, nat.bend/add_div_left_sym, nat.bend/add_sub_of_le, nat.bend/div_eq_zero_of_le, nat.bend/div_le_div, nat.bend/div_mod_eq, nat.bend/div_mod_eq_sym, nat.bend/internal_div_add_zero_r, nat.bend/internal_div_block_start, nat.bend/internal_div_block_step, nat.bend/internal_div_go_d_ge, nat.bend/internal_div_go_eq, nat.bend/internal_div_go_run, nat.bend/internal_div_go_shift, nat.bend/internal_div_go_small, nat.bend/internal_div_gt_add, nat.bend/internal_div_le_add_cancel, nat.bend/internal_div_le_big, nat.bend/internal_div_le_refl, nat.bend/internal_div_le_small, nat.bend/internal_div_le_step, nat.bend/internal_div_le_succ_r, nat.bend/internal_div_le_wit, nat.bend/internal_div_mono_go, nat.bend/internal_div_mono_wit, nat.bend/internal_div_not_succ_le, nat.bend/internal_div_true_ne_false, nat.bend/internal_div_wit_succ, nat.bend/internal_div_zero_le, nat.bend/internal_div_zero_of_wit, nat.bend/internal_lt_sub_zero, nat.bend/internal_or_false_sym, nat.bend/internal_or_true_sym, nat.bend/le_div_iff_mul_le, nat.bend/le_div_iff_mul_le_sym, nat.bend/le_of_add_eq, nat.bend/le_of_not_lt, nat.bend/lt_max_iff, nat.bend/lt_max_iff_sym, nat.bend/lt_min, nat.bend/lt_of_not_le, nat.bend/lt_sub_iff_add_lt, nat.bend/lt_sub_iff_add_lt_sym, nat.bend/min_le_iff, nat.bend/min_le_iff_sym, nat.bend/mul_le_mul_right, nat.bend/not_le_of_lt, nat.bend/not_lt_of_le, nat.bend/sub_eq_zero_of_le, nat.bend/succ_sub, order.bend/internal_or_of_false_right, order.bend/le_antisymm_eq, order.bend/le_total_of_not_le, order.bend/le_total_true, order.bend/le_total_true_sym, order.bend/le_trans3, order.bend/le_trans4, sort.bend/internal_evens_sorted, sort.bend/internal_le_trans_nat, sort.bend/internal_least, sort.bend/internal_least_cons_le, sort.bend/internal_least_cons_tail, sort.bend/internal_least_evens, sort.bend/internal_least_intro, sort.bend/internal_least_merge, sort.bend/internal_least_merge_pick, sort.bend/internal_least_odds, sort.bend/internal_least_trans, sort.bend/internal_length_evens_le, sort.bend/internal_length_odds_le, sort.bend/internal_length_zero, sort.bend/internal_merge_sorted_pick, sort.bend/internal_odds_sorted, sort.bend/internal_sorted_cons_of_least, sort.bend/internal_sorted_least_head, sort.bend/internal_sorted_short, sort.bend/merge_by_sorted, sort.bend/merge_by_sorted_nat, sort.bend/msort_by_sorted, sort.bend/msort_by_sorted_nat, sort.bend/sort_by_sorted, sort.bend/sort_by_sorted_nat, string.bend/append_assoc, string.bend/append_assoc_sym, string.bend/append_nil, string.bend/append_nil_sym, string.bend/char_cmp_refl, string.bend/char_cmp_refl_sym, string.bend/char_eq_of_is_eq, string.bend/cmp_refl, string.bend/cmp_refl_sym, string.bend/eq_of_eq_true, string.bend/eq_refl, string.bend/eq_refl_sym, string.bend/internal_append_assoc, string.bend/internal_append_nil, string.bend/internal_char_cmp_refl, string.bend/internal_cmp_refl, string.bend/internal_false_ne_true, string.bend/internal_fin_head, string.bend/internal_fin_tail, string.bend/internal_is_eq_of, string.bend/internal_length_append, string.bend/internal_rec_is_eq, string.bend/internal_reverse_append, string.bend/internal_reverse_go_spec, string.bend/internal_reverse_reverse, string.bend/internal_step, string.bend/internal_u32_cmp_refl, string.bend/internal_word_cmp_refl, string.bend/internal_word_eq, string.bend/length_append, string.bend/length_append_sym, string.bend/nil_append, string.bend/nil_append_sym, string.bend/reverse_append, string.bend/reverse_append_sym, string.bend/reverse_go_spec, string.bend/reverse_go_spec_sym, string.bend/reverse_reverse, string.bend/reverse_reverse_sym, string.bend/u32_cmp_refl, string.bend/u32_cmp_refl_sym, string.bend/u32_eq_of_is_eq; changed: list.bend/sorted_cons_cons_elim_le, list.bend/sorted_cons_cons_intro, sort.bend/insert_by_sorted, sort.bend/internal_cons_ins_step, sort.bend/internal_insert_step, sort.bend/internal_sorted_cons_cons_elim_le, sort.bend/internal_sorted_cons_cons_elim_tail, sort.bend/internal_sorted_cons_cons_intro, sort.bend/internal_sorted_cons_ins, sort.bend/internal_sorted_single, sort.bend/internal_sorted_tail, sort.bend/isort_by_sorted, sort.bend/isort_by_sorted_nat breaking
• 0.4.0.0 → 0.5.0.0: added: bool.bend/and_eq_true, bool.bend/eq_false_of_not_eq_true, bool.bend/eq_true_of_and_left, bool.bend/eq_true_of_and_right, bool.bend/eq_true_of_or_eq_false_left, bool.bend/eq_true_of_or_eq_false_right, bool.bend/false_ne_true, nat.bend/add_le_add, nat.bend/add_le_add_iff_left, nat.bend/add_le_add_iff_left_sym, nat.bend/add_le_add_right, nat.bend/le_and_le_sub_iff_add_le, nat.bend/le_and_le_sub_iff_add_le_sym; changed: list.bend/sorted_cons_cons_elim_le, list.bend/sorted_cons_cons_intro, nat.bend/internal_div_go_d_ge, nat.bend/internal_div_go_eq, nat.bend/internal_div_go_shift, nat.bend/internal_div_go_small, nat.bend/internal_div_mono_go, sort.bend/insert_by_sorted, sort.bend/internal_cons_ins_step, sort.bend/internal_evens_sorted, sort.bend/internal_insert_step, sort.bend/internal_least_evens, sort.bend/internal_least_merge, sort.bend/internal_least_merge_pick, sort.bend/internal_least_odds, sort.bend/internal_length_evens_le, sort.bend/internal_length_odds_le, sort.bend/internal_merge_sorted_pick, sort.bend/internal_odds_sorted, sort.bend/internal_sorted_cons_cons_elim_le, sort.bend/internal_sorted_cons_cons_elim_tail, sort.bend/internal_sorted_cons_cons_intro, sort.bend/internal_sorted_cons_ins, sort.bend/internal_sorted_cons_of_least, sort.bend/internal_sorted_least_head, sort.bend/internal_sorted_short, sort.bend/internal_sorted_single, sort.bend/internal_sorted_tail, sort.bend/isort_by_sorted, sort.bend/isort_by_sorted_nat, sort.bend/merge_by_sorted, sort.bend/merge_by_sorted_nat, sort.bend/msort_by_sorted, sort.bend/msort_by_sorted_nat, sort.bend/sort_by_sorted, sort.bend/sort_by_sorted_nat, string.bend/internal_rec_is_eq, string.bend/internal_step breaking
• 0.5.0.0 → 0.6.0.0: added: list.bend/all_filter, list.bend/all_filter_sym, list.bend/all_map, list.bend/all_map_sym, list.bend/all_reverse, list.bend/all_reverse_sym, list.bend/any_filter, list.bend/any_filter_sym, list.bend/any_map, list.bend/any_map_sym, list.bend/any_reverse, list.bend/any_reverse_sym, list.bend/contains_reverse, list.bend/contains_reverse_sym, list.bend/drop_append, list.bend/drop_append_of_le_length, list.bend/drop_append_of_le_length_sym, list.bend/drop_append_sym, list.bend/drop_left, list.bend/drop_left_sym, list.bend/drop_replicate, list.bend/drop_replicate_sym, list.bend/filter_false, list.bend/filter_false_sym, list.bend/filter_filter, list.bend/filter_filter_sym, list.bend/filter_true, list.bend/filter_true_sym, list.bend/foldl_map, list.bend/foldl_map_sym, list.bend/foldr_map, list.bend/foldr_map_sym, list.bend/internal_all_filter_put, list.bend/internal_all_reverse_go, list.bend/internal_any_filter_put, list.bend/internal_any_reverse_go, list.bend/internal_contains_reverse_go, list.bend/internal_filter_put_filter, list.bend/internal_replicate_append_cons, list.bend/internal_replicate_append_nil, list.bend/internal_reverse_go_replicate, list.bend/length_tail, list.bend/length_tail_sym, list.bend/length_take_le, list.bend/map_drop, list.bend/map_drop_sym, list.bend/map_id, list.bend/map_id_sym, list.bend/map_take, list.bend/map_take_sym, list.bend/replicate_add, list.bend/replicate_add_sym, list.bend/reverse_replicate, list.bend/reverse_replicate_sym, list.bend/take_append, list.bend/take_append_of_le_length, list.bend/take_append_of_le_length_sym, list.bend/take_append_sym, list.bend/take_left, list.bend/take_left_sym, list.bend/take_replicate, list.bend/take_replicate_sym, nat.bend/add_mod_left, nat.bend/add_mod_left_sym, nat.bend/add_sub_add_left, nat.bend/add_sub_add_left_sym, nat.bend/add_sub_add_right, nat.bend/add_sub_add_right_sym, nat.bend/add_sub_assoc, nat.bend/div_le_self, nat.bend/div_mul_le_self, nat.bend/div_one, nat.bend/div_one_sym, nat.bend/div_self, nat.bend/div_self_sym, nat.bend/internal_and_false_sym, nat.bend/internal_and_true_sym, nat.bend/internal_div_go_one, nat.bend/internal_div_go_self, nat.bend/internal_div_le_self_eq, nat.bend/internal_mod_eq_of_wit, nat.bend/internal_mod_go_d, nat.bend/internal_mod_go_le, nat.bend/internal_mod_go_small, nat.bend/le_add_left, nat.bend/le_min, nat.bend/le_min_sym, nat.bend/max_eq_left, nat.bend/max_eq_right, nat.bend/max_le, nat.bend/max_le_sym, nat.bend/min_eq_left, nat.bend/min_eq_right, nat.bend/mod_add_div, nat.bend/mod_add_div_sym, nat.bend/mod_eq_of_lt, nat.bend/mod_le, nat.bend/mod_lt, nat.bend/mod_mod, nat.bend/mod_mod_sym, nat.bend/mod_one, nat.bend/mod_one_sym, nat.bend/mod_self, nat.bend/mod_self_sym, nat.bend/mul_div_cancel, nat.bend/mul_div_cancel_left, nat.bend/mul_div_cancel_left_sym, nat.bend/mul_div_cancel_sym, nat.bend/mul_le_mul, nat.bend/mul_le_mul_left, nat.bend/mul_left_comm, nat.bend/mul_left_comm_sym, nat.bend/mul_mod_left, nat.bend/mul_mod_left_sym, nat.bend/mul_mod_right, nat.bend/mul_mod_right_sym, nat.bend/mul_mul_mul_comm, nat.bend/mul_mul_mul_comm_sym, nat.bend/mul_pow, nat.bend/mul_pow_sym, nat.bend/mul_right_comm, nat.bend/mul_right_comm_sym, nat.bend/mul_sub, nat.bend/mul_sub_sym, nat.bend/one_le_pow, nat.bend/pow_mul, nat.bend/pow_mul_sym, nat.bend/pow_pos, nat.bend/sub_mul, nat.bend/sub_mul_sym, nat.bend/sub_sub_self, nat.bend/zero_div, nat.bend/zero_div_sym, nat.bend/zero_mod, nat.bend/zero_mod_sym, nat.bend/zero_pow, nat.bend/zero_pow_sym; changed: list.bend/sorted_cons_cons_elim_le, list.bend/sorted_cons_cons_intro, sort.bend/insert_by_sorted, sort.bend/internal_cons_ins_step, sort.bend/internal_evens_sorted, sort.bend/internal_insert_step, sort.bend/internal_least_evens, sort.bend/internal_least_merge, sort.bend/internal_least_merge_pick, sort.bend/internal_least_odds, sort.bend/internal_length_evens_le, sort.bend/internal_length_odds_le, sort.bend/internal_merge_sorted_pick, sort.bend/internal_odds_sorted, sort.bend/internal_sorted_cons_cons_elim_le, sort.bend/internal_sorted_cons_cons_elim_tail, sort.bend/internal_sorted_cons_cons_intro, sort.bend/internal_sorted_cons_ins, sort.bend/internal_sorted_cons_of_least, sort.bend/internal_sorted_least_head, sort.bend/internal_sorted_short, sort.bend/internal_sorted_single, sort.bend/internal_sorted_tail, sort.bend/isort_by_sorted, sort.bend/isort_by_sorted_nat, sort.bend/merge_by_sorted, sort.bend/merge_by_sorted_nat, sort.bend/msort_by_sorted, sort.bend/msort_by_sorted_nat, sort.bend/sort_by_sorted, sort.bend/sort_by_sorted_nat breaking
• 0.6.0.0 → 0.7.0.0: added: list.bend/all_eq_not_any_not, list.bend/all_eq_not_any_not_sym, list.bend/any_eq_not_all_not, list.bend/any_eq_not_all_not_sym, list.bend/filter_reverse, list.bend/filter_reverse_sym, list.bend/find_append, list.bend/find_append_sym, list.bend/foldl_reverse, list.bend/foldl_reverse_sym, list.bend/foldr_cons_nil, list.bend/foldr_cons_nil_sym, list.bend/foldr_reverse, list.bend/foldr_reverse_sym, list.bend/get_cons_succ, list.bend/get_cons_succ_sym, list.bend/get_cons_zero, list.bend/get_cons_zero_sym, list.bend/get_map, list.bend/get_map_sym, list.bend/get_set_self, list.bend/get_set_self_sym, list.bend/head_append, list.bend/head_append_sym, list.bend/head_cons, list.bend/head_cons_sym, list.bend/head_map, list.bend/head_map_sym, list.bend/head_reverse, list.bend/head_reverse_sym, list.bend/internal_and_not_eq_not_or_not, list.bend/internal_find_put_or, list.bend/internal_foldl_reverse_go, list.bend/internal_foldr_reverse_go, list.bend/internal_head_reverse_go, list.bend/internal_is_empty_reverse_go, list.bend/internal_last_go_append_singleton, list.bend/internal_last_reverse_go, list.bend/internal_or_not_eq_not_and_not, list.bend/internal_range_go_append, list.bend/internal_reverse_filter_put, list.bend/is_empty_append, list.bend/is_empty_append_sym, list.bend/is_empty_iff_length_eq_zero, list.bend/is_empty_iff_length_eq_zero_sym, list.bend/is_empty_map, list.bend/is_empty_map_sym, list.bend/is_empty_reverse, list.bend/is_empty_reverse_sym, list.bend/last_append_singleton, list.bend/last_append_singleton_sym, list.bend/last_reverse, list.bend/last_reverse_sym, list.bend/length_set, list.bend/length_set_sym, list.bend/range_succ, list.bend/range_succ_sym, list.bend/tail_map, list.bend/tail_map_sym, list.bend/zip_nil_left, list.bend/zip_nil_left_sym, list.bend/zip_nil_right, list.bend/zip_nil_right_sym, maybe.bend/maybe_bind_map, maybe.bend/maybe_bind_map_sym, maybe.bend/maybe_bind_none, maybe.bend/maybe_bind_none_sym, maybe.bend/maybe_default_map, maybe.bend/maybe_default_map_sym, maybe.bend/maybe_is_none_map, maybe.bend/maybe_is_none_map_sym, maybe.bend/maybe_is_some_map, maybe.bend/maybe_is_some_map_sym, maybe.bend/maybe_map_bind, maybe.bend/maybe_map_bind_sym, maybe.bend/maybe_map_eq_bind, maybe.bend/maybe_map_eq_bind_sym, maybe.bend/maybe_map_id, maybe.bend/maybe_map_id_sym, maybe.bend/maybe_or_assoc, maybe.bend/maybe_or_assoc_sym, maybe.bend/maybe_or_none, maybe.bend/maybe_or_none_sym, nat.bend/add_lt_add, nat.bend/add_lt_add_iff_left, nat.bend/add_lt_add_iff_left_sym, nat.bend/add_lt_add_iff_right, nat.bend/add_lt_add_iff_right_sym, nat.bend/add_lt_add_left, nat.bend/add_lt_add_right, nat.bend/add_mul_div_left, nat.bend/add_mul_div_left_sym, nat.bend/add_mul_div_right, nat.bend/add_mul_div_right_sym, nat.bend/add_mul_mod_self_left, nat.bend/add_mul_mod_self_left_sym, nat.bend/add_mul_mod_self_right, nat.bend/add_mul_mod_self_right_sym, nat.bend/div_add_mod, nat.bend/div_add_mod_sym, nat.bend/internal_lt_mul_two_add, nat.bend/internal_lt_of_not_le, nat.bend/internal_lt_one_succ, nat.bend/internal_lt_two, nat.bend/le_iff_lt_or_eq, nat.bend/le_iff_lt_or_eq_sym, nat.bend/le_max_iff, nat.bend/le_max_iff_sym, nat.bend/le_max_of_le_left, nat.bend/le_max_of_le_right, nat.bend/le_mul_of_pos_left, nat.bend/le_mul_of_pos_right, nat.bend/le_of_lt_succ, nat.bend/lt_add_of_pos_left, nat.bend/lt_add_of_pos_right, nat.bend/lt_add_right, nat.bend/lt_asymm, nat.bend/lt_iff_le_and_ne, nat.bend/lt_iff_le_and_ne_sym, nat.bend/lt_min_iff, nat.bend/lt_min_iff_sym, nat.bend/lt_of_add_lt_add_left, nat.bend/lt_of_add_lt_add_right, nat.bend/lt_of_mul_lt_mul_left, nat.bend/lt_of_mul_lt_mul_right, nat.bend/lt_of_succ_le, nat.bend/lt_of_succ_lt_succ, nat.bend/lt_sub_of_add_lt, nat.bend/lt_succ_iff, nat.bend/lt_succ_iff_sym, nat.bend/lt_succ_of_le, nat.bend/max_add_add_left, nat.bend/max_add_add_left_sym, nat.bend/max_add_add_right, nat.bend/max_add_add_right_sym, nat.bend/max_le_max, nat.bend/max_lt_iff, nat.bend/max_lt_iff_sym, nat.bend/max_min_distrib_left, nat.bend/max_min_distrib_left_sym, nat.bend/min_add_add_left, nat.bend/min_add_add_left_sym, nat.bend/min_add_add_right, nat.bend/min_add_add_right_sym, nat.bend/min_le_min, nat.bend/min_le_of_left_le, nat.bend/min_le_of_right_le, nat.bend/min_lt_iff, nat.bend/min_lt_iff_sym, nat.bend/min_max_distrib_left, nat.bend/min_max_distrib_left_sym, nat.bend/mod_two_eq_zero_or_one, nat.bend/mod_two_eq_zero_or_one_sym, nat.bend/mul_lt_mul_of_lt_of_lt, nat.bend/mul_lt_mul_of_pos_left, nat.bend/mul_lt_mul_of_pos_right, nat.bend/mul_self_le_mul_self, nat.bend/mul_self_lt_mul_self, nat.bend/pos_of_ne_zero, nat.bend/pow_le_pow_left, nat.bend/pow_le_pow_right, nat.bend/pow_lt_pow_left, nat.bend/pow_lt_pow_right, nat.bend/sub_le_sub_left, nat.bend/sub_le_sub_right, nat.bend/sub_lt, nat.bend/sub_pos_of_lt, nat.bend/succ_le_of_lt, nat.bend/succ_lt_succ, nat.bend/succ_pos, string.bend/from_list_to_list, string.bend/from_list_to_list_sym, string.bend/internal_is_empty_reverse_go, string.bend/internal_length_reverse_go, string.bend/is_empty_append, string.bend/is_empty_append_sym, string.bend/is_empty_iff_length_eq_zero, string.bend/is_empty_iff_length_eq_zero_sym, string.bend/is_empty_reverse, string.bend/is_empty_reverse_sym, string.bend/length_drop, string.bend/length_drop_sym, string.bend/length_reverse, string.bend/length_reverse_sym, string.bend/length_take, string.bend/length_take_sym, string.bend/length_to_list, string.bend/length_to_list_sym, string.bend/reverse_nil, string.bend/reverse_nil_sym, string.bend/reverse_singleton, string.bend/reverse_singleton_sym, string.bend/take_append_drop, string.bend/take_append_drop_sym, string.bend/to_list_append, string.bend/to_list_append_sym, string.bend/to_list_from_list, string.bend/to_list_from_list_sym; changed: list.bend/drop_append_of_le_length, list.bend/drop_append_of_le_length_sym, list.bend/length_take_le, list.bend/sorted_cons_cons_elim_le, list.bend/sorted_cons_cons_intro, list.bend/take_append_of_le_length, list.bend/take_append_of_le_length_sym, sort.bend/insert_by_sorted, sort.bend/internal_cons_ins_step, sort.bend/internal_evens_sorted, sort.bend/internal_insert_step, sort.bend/internal_least_evens, sort.bend/internal_least_merge, sort.bend/internal_least_merge_pick, sort.bend/internal_least_odds, sort.bend/internal_length_evens_le, sort.bend/internal_length_odds_le, sort.bend/internal_merge_sorted_pick, sort.bend/internal_odds_sorted, sort.bend/internal_sorted_cons_cons_elim_le, sort.bend/internal_sorted_cons_cons_elim_tail, sort.bend/internal_sorted_cons_cons_intro, sort.bend/internal_sorted_cons_ins, sort.bend/internal_sorted_cons_of_least, sort.bend/internal_sorted_least_head, sort.bend/internal_sorted_short, sort.bend/internal_sorted_single, sort.bend/internal_sorted_tail, sort.bend/isort_by_sorted, sort.bend/isort_by_sorted_nat, sort.bend/merge_by_sorted, sort.bend/merge_by_sorted_nat, sort.bend/msort_by_sorted, sort.bend/msort_by_sorted_nat, sort.bend/sort_by_sorted, sort.bend/sort_by_sorted_nat breaking
• 0.7.0.0 → 0.7.1.0: added: algebra.bend/foldl_eq_foldr, algebra.bend/foldl_eq_foldr_sym, algebra.bend/internal_foldl_assoc, algebra.bend/internal_foldl_eq_foldr, nat.bend/add_le_add_iff_right, nat.bend/add_le_add_iff_right_sym, nat.bend/add_left_cancel_iff, nat.bend/add_left_cancel_iff_sym, nat.bend/add_right_cancel_iff, nat.bend/add_right_cancel_iff_sym, nat.bend/double_add, nat.bend/double_add_sym, nat.bend/double_div_two_add_mod_two, nat.bend/double_div_two_add_mod_two_sym, nat.bend/double_eq_two_mul, nat.bend/double_eq_two_mul_sym, nat.bend/double_le_double, nat.bend/double_lt_double, nat.bend/double_mul, nat.bend/double_mul_sym, nat.bend/double_sub, nat.bend/double_sub_sym, nat.bend/le_double, nat.bend/le_min_of_le_of_le, nat.bend/max_le_of_le_of_le, nat.bend/mul_double, nat.bend/mul_double_sym, nat.bend/sub_add_comm, nat.bend/two_mul, nat.bend/two_mul_sym; changed: list.bend/drop_append_of_le_length, list.bend/drop_append_of_le_length_sym, list.bend/length_take_le, list.bend/sorted_cons_cons_elim_le, list.bend/sorted_cons_cons_intro, list.bend/take_append_of_le_length, list.bend/take_append_of_le_length_sym, sort.bend/insert_by_sorted, sort.bend/internal_cons_ins_step, sort.bend/internal_evens_sorted, sort.bend/internal_insert_step, sort.bend/internal_least_evens, sort.bend/internal_least_merge, sort.bend/internal_least_merge_pick, sort.bend/internal_least_odds, sort.bend/internal_length_evens_le, sort.bend/internal_length_odds_le, sort.bend/internal_merge_sorted_pick, sort.bend/internal_odds_sorted, sort.bend/internal_sorted_cons_cons_elim_le, sort.bend/internal_sorted_cons_cons_elim_tail, sort.bend/internal_sorted_cons_cons_intro, sort.bend/internal_sorted_cons_ins, sort.bend/internal_sorted_cons_of_least, sort.bend/internal_sorted_least_head, sort.bend/internal_sorted_short, sort.bend/internal_sorted_single, sort.bend/internal_sorted_tail, sort.bend/isort_by_sorted, sort.bend/isort_by_sorted_nat, sort.bend/merge_by_sorted, sort.bend/merge_by_sorted_nat, sort.bend/msort_by_sorted, sort.bend/msort_by_sorted_nat, sort.bend/sort_by_sorted, sort.bend/sort_by_sorted_nat breaking
• 0.7.1.0 → 0.7.2.0: added: list.bend/drop_succ, list.bend/drop_succ_sym, list.bend/length_singleton, list.bend/length_singleton_sym, list.bend/reverse_cons, list.bend/reverse_cons_sym, list.bend/take_succ, list.bend/take_succ_sym, nat.bend/min_le_max, nat.bend/min_le_max_sym, nat.bend/mul_two, nat.bend/mul_two_sym, nat.bend/pow_two, nat.bend/pow_two_sym; changed: list.bend/drop_append_of_le_length, list.bend/drop_append_of_le_length_sym, list.bend/length_take_le, list.bend/sorted_cons_cons_elim_le, list.bend/sorted_cons_cons_intro, list.bend/take_append_of_le_length, list.bend/take_append_of_le_length_sym, sort.bend/insert_by_sorted, sort.bend/internal_cons_ins_step, sort.bend/internal_evens_sorted, sort.bend/internal_insert_step, sort.bend/internal_least_evens, sort.bend/internal_least_merge, sort.bend/internal_least_merge_pick, sort.bend/internal_least_odds, sort.bend/internal_length_evens_le, sort.bend/internal_length_odds_le, sort.bend/internal_merge_sorted_pick, sort.bend/internal_odds_sorted, sort.bend/internal_sorted_cons_cons_elim_le, sort.bend/internal_sorted_cons_cons_elim_tail, sort.bend/internal_sorted_cons_cons_intro, sort.bend/internal_sorted_cons_ins, sort.bend/internal_sorted_cons_of_least, sort.bend/internal_sorted_least_head, sort.bend/internal_sorted_short, sort.bend/internal_sorted_single, sort.bend/internal_sorted_tail, sort.bend/isort_by_sorted, sort.bend/isort_by_sorted_nat, sort.bend/merge_by_sorted, sort.bend/merge_by_sorted_nat, sort.bend/msort_by_sorted, sort.bend/msort_by_sorted_nat, sort.bend/sort_by_sorted, sort.bend/sort_by_sorted_nat breaking