bend-lawful-stdlib

Releases (1)

• 0.1.0.0 indexed

Definitions (248)

src/sorted.bend

• law insert_from.go
• law insert_from
• law insert_sorted.go
• law insert_sorted
• law sort_sortedsort's output is sorted.
• def bump
• law bump_swap
• def counthow many elements of xs ~eq calls equal to y
• law insert_count.go
• law insert_count
• law sort_countsort keeps every element's count.

src/tree.bend

• type Tree
• def reduce
• def to_list.gothe leaves, left to right, in front of acc
• def to_list
• def builda balanced tree with 2^d leaves f(lo), f(lo+1), ..., so both halves of each parallel call do the same amount of work
• law reduce_foldrreduce agrees with foldr.

src/u32.bend

• def bit
• law cmp_bitscomparing bit + 2*rest compares the rests first, then the bits, which is what Word.cmp.fin does
• law Word.cmp_nat
• law cmp_nat
• def LEa <= b on U32
• law is_lt_nata result of U32.is_lt is the same result of Nat.is_lt on the numbers
• law min_le_r.go
• law min_le_rmin(a, b) <= b
• law le_max_r.go
• law le_max_rb <= max(a, b)
• law clamp_le_hiclamp(x, lo, hi) <= hi, even when lo > hi
• law lo_le_clamp.go
• law lo_le_clamplo <= clamp(x, lo, hi) when lo <= hi
• law Word.sub_add(a + b + c) - b, with carry not(c), is a.
• law Word.sub_add.armone bit: the bit is kept, and e is the law for the rest at the carry k
• law Word.add_sub(a - b) + b, with carry not(c), is a
• law Word.add_sub.armone bit: the bit is kept, and e is the law for the rest at the carry k
• law sub_addsubtracting b undoes adding b, with wraparound
• law add_subadding b undoes subtracting b, with wraparound
• def groupwrapping + and - as a C.Group

src/v2.bend

• type V2
• def add
• def sub
• law sub_add
• law add_sub
• def group

src/vec.bend

• def Vec
• def from_lista list as a Vec of its own length
• def get
• def zip_with
• def foldr