~/bend-docscommunity

proofs/containers/balanced_search_tree/nav.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/nav.bend as Nav

11 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/balanced_search_tree.bend as M
import ./state.bend as ST
import ./mirror.bend as MI
import ./tree.bend as TR
import ./path.bend as P
import ./nbr.bend as NB
import ../../lib/nat_list.bend as NL

Definitions

def best_l source · line 29 · raw

@+h:Bool -> @+i:Nat -> @+a:Nat -> @+b:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.pick(Nat, h, i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pk(Nat, h, a, b)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pk(Nat, h, i, b) : Nat}

the candidate after a step left / right

def best_r source · line 36 · raw

@+h:Bool -> @+i:Nat -> @+a:Nat -> @+b:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.pick(Nat, h, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pk(Nat, h, a, b), i) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.pk(Nat, h, a, i) : Nat}

Templates

template gnav source · line 20 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/state.Tr -> @+c:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/balanced_search_tree/path.Fr> -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> @+k:K -> @+h:Bool -> @+incl:Bool -> Nat