lawful-arrays

Releases (1)

• 0.1.0.0 indexed

Definitions (159)

defs.bend

• def fulla is a perfect tree of depth d: 2^d leaves, every one at depth d.
• def viewThe leaves of a, left to right (the same list as Base's Array.to_list, which is a template and cannot appear in a law).
• def slotThe leaf an access at index i reaches in a perfect tree of depth d < 32: i modulo 2^d.

LAWS.bend

• law new_full
• law new_view
• law view_length
• law size_countArray.size doubles 1 once per level of the left spine: for a perfect tree of depth d below 32 that is the number of leaves, 2^d.
• law size_kept
• law get_viewArray.get reads leaf i (modulo the size).
• law get_keptArray.get hands back the same array.
• law set_viewArray.set replaces leaf i (modulo the size) and nothing else.
• law set_full
• law get_set_sameReading what was just written gives it back.
• law get_set_otherWriting leaf i does not change leaf j (j a different leaf modulo the size).
• law swap_view
• law swap_old
• law swap_full
• law view_injTwo perfect trees of the same depth with the same leaves are the same array.
• law get_pairArray.get as a literal pair (so code that destructures it can be rewritten).
• law size_pair
• law get_newA new array reads as its initial value everywhere (every depth, every index).
• law slot_lt
• law slot_small
• law clone_pairArray.clone gives two arrays equal to the original.

PROOF.bend

• def full_tRewrites a fact about a into the same fact about the mirror.
• def view_length.go
• def size_count.go
• def size_pair.go
• def get_view.go
• def get_pair.go
• def get_kept.go
• def set_view.go
• def get_set_same.go
• def get_set_other.go
• def swap_view.go
• def swap_old.go
• def view_inj.go

proof_base.bend

• def substTransport along an equation.
• def Bool.disc_ft
• law false_ne_true
• law true_ne_false
• law and_true_l
• law and_true_r
• def Nat.disc_z
• law succ_ne_zero
• def pred
• law succ_inj
• law add_zero
• law add_succ
• law sub_zero
• law lt_zero
• law lt_zero_absurd
• law lt_oneBelow 1 is 0.
• law not_lt_le
• law lt_subk is at least m and below m + m2, so k - m is below m2.
• law lt0_add
• law pow_pos
• law pow_succ2^(1+p) unfolds to p' + (p' + 0); this is p' + p'.
• law lt_dbl
• law lt_one_dbl
• law pow_lt
• law length_append
• law get_append_lBefore index length(xs), xs ++ ys reads like xs.
• law get_append_rFrom index length(xs) on, xs ++ ys reads like ys.
• law set_append_l
• law set_append_r
• law replicate_add
• law get_set_neWriting index i does not change index j != i.
• def head_or
• def tail
• law cons_inj_h
• law cons_inj_t
• law append_inj_lTwo appends with equally long first parts: the first parts are equal...
• law append_cancel_l...and so are the second parts.

proof_index.bend

• law n_half
• law half
• law lo_idx
• law hi_nlt
• law le_shr
• law hi_sub
• law hi_idx
• law gg
• law gsoWhat a swap hands back is the leaf it replaced.
• law gsvA swap writes leaf i of the list of leaves.
• law one_mul
• law size_n
• law le0
• law le1_pow
• def le1_pow.go
• law le1
• law mask_n
• law slot_n
• law slot_lt_t
• law slot_small_t
• law jlt
• law size_count_t
• law get_view_t
• law swap_old_t
• law swap_view_t
• law set_view_t