lawful-arrays
Releases (1)
-
0.1.0.0 indexed
Definitions (159)
proof_index.bend
- def tswapThe tree a swap leaves, as a Tree (so the written array has a mirror too).
- law tswap_eq
- def set_tree
- law set_tree_eq
- def unsome
- law get_set_other_t
proof_shape.bend
- def SizeWArray.size(a) is (b, n) with b == a.
- law size_node_eq
- def size_w.node
- def size_w
- def SwapWArray.swap.go(a, ...) is (na, old) with na as perfect as a at every depth.
- law lo_eq
- law hi_eq
- law and_eq_l
- law and_eq_r
- def swap_w.lo
- def swap_w.hi
- def swap_w
- def swap_full.finThe array a swap leaves is perfect: the steps after Array.size.
- def swap_full.go
- law swap_full
- def set_full.fin
- def set_full.go
- law set_full
proof_tree.bend
- type Tree
- def fromT
- def Mirror
- law anode_eq
- def mirror.node
- def mirror
- law lo_fst
- law lo_snd
- law hi_fst
- law hi_snd
- law fin_fst
- law size_eta
- law size_tree
- law view_length
- law new_full
- law new_view
- law get_new_go
- law clone_pair
- law get_go_eta
- law get_pair_t
- law sz_swA swap keeps the left spine, so the size.
- law gssReading where a swap wrote gives the written value (any tree).
- law get_set_same_t
- law view_inj_t
- law get_new_t
proof_words.bend
- law w_shr
- law w_lt
- law w_le
- law w_sub_le
- law w_and_mask
- law w_shln_fits
- law n_mod_lt
- law n_mod_small
- law n_div_mul_add
- law n_mul_comm