bend-collections-laws-math

Releases (1)

• 1.0.0.0 indexed

Definitions (5,526)

proofs/lib/lemmas/src/cache.bend

• def purge_loopNo accumulated event log is stored in the cache itself.
• def purge
• def first_entry
• def oldest_entry
• def finite_entry
• def purge_needs_clockOne oldest inspection.
• def collect_entry
• def entries_go
• def entriesRaw enumeration.
• def map_size

proofs/lib/lemmas/src/time.bend

• def add
• def milliseconds
• def is_zero
• def deadline_choose
• def deadline
• def le
• def expired_choose
• def expired

proofs/lib/lemmas/src/wide.bend

• def zeroAll bits are represented explicitly: no Nat holds a full-width integer.
• def inc
• def add
• def neg
• def last
• def is_zero
• def signed_order
• def le
• def bit_u32
• type Division
• def digit_result
• def digit_compare
• def digit
• def div_millionBinary long division, processing the most significant bit first.
• def quotient
• def unsigned_milliseconds
• def signed_milliseconds
• def milliseconds
• def joinExact limb boundary used by the host bridge; limbs themselves are primitive U32.
• type Parts
• def split_cons
• def split
• def pack
• def limbs
• def unpack

proofs/lib/lemmas/types/model.bend

• type IntegerNegative{n} denotes -(n+1), so zero has exactly one representation.
• type Int64
• type Metrics
• type Entry
• type LruEvent
• def zero_metrics

proofs/lib/list.bend

• def cons_cong
• def append_nil
• def append_assoc
• def length_append
• def snoc_append
• def length_snoc
• def length_replicate
• def replicate_add
• def nth_append_left
• def nth_append_right
• def update_append_left
• def update_append_right
• def length_update
• def nth_lt_length
• def nth_update_same
• def nth_none
• def base_appendBase List.append agrees with the specification append.
• def length_zero_nil
• def rev_go_twicereverse.go(reverse.go(xs, a), b) == reverse.go(a, xs ++ b)
• def rev_rev
• def nth_update_other
• def append_snoc
• def snoc_append_cons
• def rev_snoc
• def spec_rev_rev
• def rev_append
• def length_rev
• def base_rev_go
• def base_rev
• def base_take_drop
• def length_take
• def length_drop
• def last_snoc
• def init_snoc
• def sc_length_take
• def sc_nth_take
• def sc_take_take
• def sc_take_zero
• def sc_take_append_left
• def sc_take_append_right
• def sub_zero_eqtake r == take l ++ (next r - l after l), for l <= r
• def sc_take_split
• def sc_drop_takedrop l (take n xs) == take (n - l) (drop l xs)
• def sc_take_update
• def sc_take_rep
• def sc_nth_somenth below the length is not None

proofs/lib/logic.bend

• def truth
• def false_true
• def true_false
• def and_left
• def and_right