bend-kit-collections
Releases (6)
Definitions (620)
LAWS.bend
- def scmp.fin
- def scmp
- def m3
- def m7.go
- def m7
- law omap_keys_ascending_puts
- law omap_size_del
- law omap_get_after_rotations
- law omap_keys_del_root
- law omap_get_put
- law omap_get_put_replace
- law omap_get_put_other
- law omap_get_missing
- law omap_keys_sorted
- law omap_size_replace
- law omap_get_del
- law omap_get_del_other
- law omap_keys_del
- law omap_string_keys
- law oset_to_list
- law oset_has_del
- def flipThe laws below hold for every comparator that is a total order, with EQ meaning equal keys.
- def above
- def below
- def boundedEvery key of m lies strictly between the bounds, in search-tree order.
- def searchtree
- def sorted.go
- def sorted
- law omap_new_searchtree
- law omap_put_searchtree
- law omap_del_searchtree
- law omap_searchtree_keys_sorted
- law omap_get_put_same
- law omap_get_put_other_key
- law order_string_reflOrder.string is a total order with EQ meaning equal strings: it meets the refl, eq, flip and trans facts that the OMap laws above take.
- law order_string_eq
- law order_string_flip
- law order_string_trans
- law order_string_fixturesLower code points first, and a prefix before its extensions.
- def omap_weightGhost weight from tree shape: weight = stored size + 1, so OTip has weight 1 and OBin{lo, hi} has weight w(lo) + w(hi).
- def weight_ok
- def weight_balanced
- def g_heavy_hiThe ghost map below has the shape of OMap: it builds nodes with the same OMap.bin and rotations, but it compares Nat weights where OMap compares U32 sizes.
- def g_heavy_lo
- def g_rot_lo
- def g_rot_hi
- def g_balance.if
- def g_balance
- def g_put
- def g_pop_min.fin
- def g_pop_min
- def g_glue.fin
- def g_glue
- def g_del
- law omap_new_weight_balanced
- law omap_g_put_matches
- law omap_g_del_matches
- law omap_put_weight_balanced
- law omap_del_weight_balanced
- law vec_from_list
- law vec_get
- law vec_get_past_len
- law vec_set
- law vec_pop
- law vec_pop_empty
- law vec_pop_to_list
- law deque_ends
- law heap_sort
- def hkey
- def hm
- law hmap_get_put
- law hmap_get_put_other
- law hmap_collision
- law hmap_replace_collision
- def full
- law hmap_high_bit
- law hmap_missing_collision
- def hmap_absentNo entry of xs has a key equal to k.
- def hmap_distinctNo two entries of xs have equal keys.
- def hmap_hashedEvery key of xs hashes to h.
- def hmap_wf.goA trie with n levels left: buckets hold distinct keys; above the last level, a bucket's keys hash to its hash; the last level has no branches.
- def hmap_wf
- law hmap_new_wf
- law hmap_put_wf
- law hmap_del_wf
- law hmap_get_put_same
- law hmap_get_put_other_key
- law hmap_get_del_same
- law hmap_get_del_other_key
- law hmap_size_put_new
- law hmap_size_put_replace
- law hmap_size_del
- law hmap_size_del_missing
- law hmap_collision_getTwo distinct keys with one hash share a bucket; both stay reachable.
- law hmap_collision_size