bend-kit-collections

Search uses release 0.1.4.1 · 620 definitions

Releases (6)

0.1.4.1 indexed
0.1.4.0 unindexed
0.1.3.0 unindexed
0.1.2.0 unindexed
0.1.1.0 unindexed
0.1.0.0 unindexed

Definitions (620)

deque.bend

type Deque
def Deque.new
def Deque.from_listthe list's first element is the deque's front
def Deque.push_front
def Deque.push_back
def Deque.count.put
def Deque.counta list and its length, in one pass that hands the list back
def Deque.half
def Deque.split.put
def Deque.splitthe first n elements, and the rest
def Deque.pop_front.go
def Deque.pop_front.halves
def Deque.pop_front.refill
def Deque.pop_front
def Deque.pop_back.go
def Deque.pop_back.halves
def Deque.pop_back.refill
def Deque.pop_back
def Deque.to_listthe elements, front to back
def Deque.length
def Deque.is_empty

PROOF.bend

def h.u_ne0.cRouting facts about hashes and a mask.
def h.u_ne0
def h.u_route_t.c
def h.u_route_t
def h.u_same0
def h.u_diff.c
def h.u_diff
def h.g_loUnfolding get.go by a known test, simple side first.
def h.g_hi
def h.g_lf_t
def h.gnil
def h.g_nil_leaf
def h.get_leaf
def h.size_leaf
def h.get_join
def h.size_join
def h.wf_nil
def h.wf_leaf
def h.wf_join
def h.fresh_getget after put, same key.
def h.split_same.b
def h.split_same
def h.gp_same.lf
def h.gp_same.br
def h.gp_same
def h.r_eg.cget after put, other key.
def h.r_eg
def h.r_none
def h.g_leaf_r
def h.g_fresh_none
def h.split_other.b
def h.split_other
def h.gp_other.lf
def h.gp_other.br
def h.gp_other
def h.gd_same.lfget after del.
def h.gd_same.br
def h.gd_same
def h.gd_other.lf
def h.gd_other.br
def h.gd_other
def h.split_size.bsize after put and del.
def h.split_size
def h.sz_put_new.lf
def h.sz_put_new.br
def h.sz_put_new
def h.sz_put_hit.lf
def h.sz_put_hit.br
def h.sz_put_hit
def h.sz_del_hit.lf
def h.sz_del_hit.br
def h.sz_del_hit
def h.sz_del_miss.lf
def h.sz_del_miss.br
def h.sz_del_miss
def h.wf_freshput and del keep the map well formed.
def h.wf_leaf_o
def h.split_wf.b
def h.split_wf
def h.wf_put.lf
def h.wf_put.br
def h.wf_put
def h.wf_del.lf
def h.wf_del.br
def h.wf_del
def lt_absurdA comparison equal to LT is not one whose is_lt is False.
def ncmp_refl
def ncmp_eq
def ncmp_flip
def ncmp_trans
def ucmp_nat
def ucmp_refl
def ucmp_eq
def ucmp_flip
def ucmp_lt
def ucmp_trans
def seq.stepOne step of eq on the heads a and b, with the tails' result as ih.
def sfin_flip
def strans.stepOne step of transitivity on the heads a < b < c, with the tails' result as ih.