bend-collections-laws-math
Releases (1)
-
1.0.0.0 indexed
Definitions (5,526)
proofs/lib/logic.bend
- def and_intro
- def not_true
- def not_false
- def bool_cases
- def true_not_false
- def cmp_codeCmp discrimination.
- def cmp_lt_eq
- def cmp_lt_gt
- def cmp_eq_gt
- def none_someMaybe discrimination.
- def some_value
- def some_inj
- def pair_fst
- def pair_snd
- def pair_eq
- def substTransport a proof along an equation.
- def sfstDependent pair projections (call results cannot be destructured directly).
- def ssnd
- def pair_eta
proofs/lib/nat.bend
- def pred
- def succ_inj
- def succ_cong
- def is_zero
- def zero_succ
- def succ_zero
- def add_zero
- def add_succ
- def add_comm
- def add_assoc
- def lt_irrefl
- def le_refl
- def lt_succ
- def le_succ
- def zero_le
- def not_lt_zero
- def lt_zero_absurd
- def lt_le
- def le_lt_succ
- def lt_succ_le
- def succ_le_lt
- def lt_succ_le_succ
- def le_trans
- def lt_le_trans
- def le_lt_trans
- def lt_trans
- def not_lt_leis_lt(a, b) == False gives b <= a.
- def le_not_lt
- def lt_not_le
- def not_le_lt
- def lt_asym
- def le_antisym
- def eq_le
- def lt_ne
- def eq_from_is_eq
- def is_eq_refl
- def is_eq_lt
- def lt_or_eq
- def add_sub_cancel
- def sub_add
- def sub_zero
- def sub_self
- def sub_succ_left
- def sub_lt
- def le_add_right
- def lt_add_left
- def le_add_left
- def double_inj
- def even_odd
- def bit_split_bitbit + 2u == bit' + 2v determines both parts.
- def bit_split_val
- def double_lt
- def double_le
- def bit_double_ltbit + 2u < 2v gives u < v.
- def double_lt_bit
- def double_self_le
- def double_succ_le
- def pow2_pos
- def pow2_lt_succ
- def pow2_mono1 <= n gives 1 + n <= 2n.
- def pow2_strict
- def pred_doublepred(2v) == 1 + 2 pred(v) for v >= 1.
- def add_double
- def bump2
- def acc2
- def peel2
- def fst_bump2
- def div2_step
- def double_succ
- def div2_double
- def div2_pow22^(1+r) / 2 = 2^r
- def min_left
- def min_right
- def is_eq_sym_false
- def lt_add_r2a < b ==> a + c < b + c