bend-mathlib

Search uses release 0.8.1.0 · 1,126 definitions

Releases (15)

0.8.1.0 indexed
0.8.0.0 unindexed
0.7.5.0 unindexed
0.7.4.0 unindexed
0.7.3.0 unindexed
0.7.2.0 unindexed
0.7.1.0 unindexed
0.7.0.0 unindexed
0.6.0.0 unindexed
0.5.0.0 unindexed
0.4.0.0 unindexed
0.3.0.0 unindexed
0.2.0.0 unindexed
0.1.0.1 unindexed
0.1.0.0 unindexed

Definitions (1,126)

string.bend

law is_empty_reverse_symThe reverse is empty exactly when the string is, reversed to rewrite toward the simple side.
law take_append_drop_symTaking n characters and appending the rest after dropping n gives the string back, reversed to rewrite toward the simple side.
law length_take_symTaking n characters leaves min(n, length) of them, reversed to rewrite toward the simple side.
law length_drop_symDropping n characters leaves length - n of them, reversed to rewrite toward the simple side.
law to_list_from_list_symConverting a character list to a string and back gives the list, reversed to rewrite toward the simple side.
law from_list_to_list_symConverting a string to a character list and back gives the string, reversed to rewrite toward the simple side.
law to_list_append_symThe characters of an append are the characters of each part, appended, reversed to rewrite toward the simple side.
law length_to_list_symA string has as many characters as its character list, reversed to rewrite toward the simple side.

u32.bend

def internal_succ_double_lt
law word_to_nat_ltA word's value is below two to the width: to_nat w < 2^n.
law word_to_nat_zeroThe zero word is the natural zero: to_nat (zero n) = 0.
law word_to_nat_injDistinct words have distinct values: to_nat a = to_nat b implies a = b.
def internal_bv
def internal_to_nat_con
def internal_cmp_bits
law word_cmp_to_natComparing words compares their values: cmp a b = cmp (to_nat a) (to_nat b).
law word_not_addOne plus a word plus its complement is two to the width: 1 + to_nat (not w) + to_nat w = 2^n.
def internal_pick_pow
def internal_carry
def internal_full_add
def internal_adc_nat
def internal_adc_core
def internal_lt_congl
def internal_le_congr
def internal_fin_exact
def internal_fin_wrap
def internal_fin_over
law word_adc_exactThe adder is exact below the overflow: a + b + carry-in < 2^n implies to_nat (adc a b False c) = a + b + carry-in.
law word_adc_overflowThe adder drops exactly one 2^n on overflow: 2^n <= a + b + carry-in implies to_nat (adc a b False c) + 2^n = a + b + carry-in.
law word_adc_wrapThe adder wraps modulo 2^n: to_nat (adc a b False c) = (a + b + carry-in) % 2^n.
law word_add_exactWord addition is exact without overflow: a + b < 2^n implies to_nat (add a b) = a + b.
law word_add_wrapWord addition wraps modulo 2^n: to_nat (add a b) = (a + b) % 2^n.
def internal_inc_carry
def internal_inc_core
law word_inc_exactIncrement is exact without overflow: 1 + w < 2^n implies to_nat (inc w) = 1 + w.
law word_inc_wrapIncrement wraps modulo 2^n: to_nat (inc w) = (1 + w) % 2^n.
def internal_adc_not
def internal_sub_arith
law word_sub_exactWord subtraction is exact without underflow: b <= a implies to_nat (sub a b) = a - b.
def internal_sub_wrap_arith
law word_sub_wrapWord subtraction wraps modulo 2^n: to_nat (sub a b) = (a + (2^n - b)) % 2^n.
def internal_bound
def internal_u32_to_nat_lt
law u32_to_nat_ltA U32's value is below 2^32.
law u32_to_nat_injDistinct U32s have distinct values: to_nat a = to_nat b implies a = b.
law u32_cmp_to_natComparing U32s compares their values: cmp a b = cmp (to_nat a) (to_nat b).
law u32_is_eq_to_natU32 equality tests the values: is_eq a b = is_eq (to_nat a) (to_nat b).
law u32_is_ne_to_natU32 disequality tests the values: is_ne a b = is_ne (to_nat a) (to_nat b).
law u32_is_lt_to_natThe U32 strict order is the order of the values: is_lt a b = is_lt (to_nat a) (to_nat b).
law u32_is_le_to_natThe U32 order is the order of the values: is_le a b = is_le (to_nat a) (to_nat b).
law u32_is_gt_to_natThe reverse U32 strict order is that of the values: is_gt a b = is_gt (to_nat a) (to_nat b).
law u32_is_ge_to_natThe reverse U32 order is that of the values: is_ge a b = is_ge (to_nat a) (to_nat b).
def internal_u32_add_exact
law u32_add_exactU32 addition is exact without overflow: a + b < 2^32 implies to_nat (a + b) = a + b.
def internal_u32_add_wrap
law u32_add_wrapU32 addition wraps modulo 2^32: to_nat (a + b) = (a + b) % 2^32.
law u32_sub_exactU32 subtraction is exact without underflow: b <= a implies to_nat (a - b) = a - b.
def internal_u32_sub_wrap
law u32_sub_wrapU32 subtraction wraps modulo 2^32: to_nat (a - b) = (a + (2^32 - b)) % 2^32.
def internal_u32_inc_exact
law u32_inc_exactU32 increment is exact without overflow: 1 + a < 2^32 implies to_nat (inc a) = 1 + a.
def internal_u32_inc_wrap
law u32_inc_wrapU32 increment wraps modulo 2^32: to_nat (inc a) = (1 + a) % 2^32.
def internal_u32_to_nat_from_nat
law u32_to_nat_from_natConverting a natural below 2^32 to U32 and back is the identity: k < 2^32 implies to_nat (from_nat k) = k.
law u32_from_nat_to_natConverting a U32 to a natural and back is the identity: from_nat (to_nat a) = a.
def internal_mod_succ_mod
def internal_u32_to_nat_from_nat_mod
law u32_to_nat_from_nat_modConverting any natural to U32 and back reduces it modulo 2^32: to_nat (from_nat k) = k % 2^32.
def internal_min_fin
law u32_min_to_natThe U32 minimum is the minimum of the values: to_nat (min a b) = min (to_nat a) (to_nat b).
def internal_max_fin
law u32_max_to_natThe U32 maximum is the maximum of the values: to_nat (max a b) = max (to_nat a) (to_nat b).
def internal_shl_val
def internal_shl_con
def internal_shl_out
def internal_shl_out32
def internal_div_step
def internal_bit_double_lt
def internal_rem_lt_add
def internal_rem_lt
def internal_wrap_sum
def internal_wrap_rem
def internal_dm_inv
def internal_dm_take
def internal_dm_wrap
def internal_dm_fin
def internal_dm_shl
def internal_dm_rec
def internal_dm_go
def internal_div_unique
def internal_div_fin
def internal_div_if
law u32_div_to_natU32 division is the division of the values, also for a zero divisor: to_nat (a / b) = to_nat a / to_nat b.
law u32_div_le_div_leftU32 division is antitone in a positive divisor: 0 < s and s <= t imply a / t <= a / s.
law word_to_nat_zero_symThe zero word is the natural zero: to_nat (zero n) = 0, reversed to rewrite toward the simple side.
law word_cmp_to_nat_symComparing words compares their values: cmp a b = cmp (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
law word_not_add_symOne plus a word plus its complement is two to the width: 1 + to_nat (not w) + to_nat w = 2^n, reversed to rewrite toward the simple side.
law word_adc_exact_symThe adder is exact below the overflow: a + b + carry-in < 2^n implies to_nat (adc a b False c) = a + b + carry-in, reversed to rewrite toward the simple side.
law word_adc_overflow_symThe adder drops exactly one 2^n on overflow: 2^n <= a + b + carry-in implies to_nat (adc a b False c) + 2^n = a + b + carry-in, reversed to rewrite toward the simple side.