bend-osdev-array

Search uses release 0.1.0.1 · 227 definitions

Releases (2)

0.1.0.1 indexed
0.1.0.0 unindexed

Definitions (227)

PROOF.bend

def AP.get_top
def AP.set_top
def AP.size_eq
def AP.swap_eq
def AP.get_eq
def AP.get_top_eq
def AP.set_top_eq
def AP.swap_size
def AP.get_swap_same
def AP.perf_swap
def AP.size_perf
def AP.new_perf
def AP.get_same_array.go
def AP.get_set_same.go
def AP.lt_zero
def AP.lt_succ_l
def AP.lt_le
def AP.double_le
def AP.dpos
def AP.slots_pos
def AP.slots_le
def AP.lt_splita value below double(s), split at s
def AP.con_cong
def AP.len_app
def AP.get_app_l
def AP.get_app_r
def AP.set_app_l
def AP.set_app_r
def AP.get_set_other
def AP.and_zero
def AP.val0
def AP.lt_bv_inv
def AP.lt_bv
def AP.mask_lta word masked to its low d bits is below 2^d
def AP.and_ida word below 2^d is unchanged by the mask
def AP.u32_mask_lt
def AP.u32_and_id
def AP.inc
def AP.u32_inc
def AP.lt_rw
def AP.from_natfrom_nat then to_nat is the identity below 2^d, d <= 32
def AP.app_cong_l
def AP.app_cong_r
def AP.lt_rw_r
def AP.lt_rw_l
def AP.lt_split2
def AP.eb_fix
def AP.lt_true
def AP.lt_false
def AP.u32_sub_add
def AP.le_rw_l
def AP.splitan index at or above 2^p, split into 2^p and the rest
def AP.len_perf
def AP.get_leaves
def AP.set_leaves
def AP.tnew
def AP.new_eq
def AP.get_v_new
def AP.rep_add
def AP.unsome
def AP.some_inj
def AP.perf_rw
def AP.index_lt
def AP.tree_perf
def AP.tree_get
def AP.tree_set
def AP.set_keeps_size.go
def AP.get_new.go
def AP.set_perfect.go.body
def AP.set_perfect.go
def AP.size_perfect.go.body
def AP.size_perfect.go
def AP.new_leaves.go
def AP.model_length.go.body
def AP.model_length.go
def AP.model_get.go.body
def AP.model_get.go
def AP.model_set.go.body
def AP.model_set.go
def AP.get_set_other.go.body
def AP.get_set_other.go
def AP.index_of_nat.go
def AP.pred
def AP.pred_cong
def AP.tof
def AP.of_list_eq
def AP.tof_perf
def AP.take_drop
def AP.take_app
def AP.drop_app
def AP.len_takea list of n + m elements cut after n: n, then m elements
def AP.len_drop
def AP.one_elem
def AP.tof_leaves
def AP.tree_exta perfect tree is the tree of its own leaves
def AP.nth_get
def AP.set_length
def AP.get_set_same
def AP.get_rep
def AP.tnew_tof