~/bend-docscommunity

proofs/containers/balanced_search_tree/nsr.bend checks

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

5 imports
import Base
import ../../../spec/lib/common.bend as SC
import ../../lib/array.bend as AR
import ../../../src/containers/balanced_search_tree.bend as M
import ./bk.bend as BK

Templates

template tags source · line 12 · raw

@-K:Data -> @xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> List<&2, Nat>

template lefts source · line 19 · raw

@-K:Data -> @xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> List<&2, Nat>

template rights source · line 26 · raw

@-K:Data -> @xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> List<&2, Nat>

template parents source · line 33 · raw

@-K:Data -> @xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> List<&2, Nat>

template keys source · line 40 · raw

@-K:Data -> @xs:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> List<&2, Maybe<&2, K>>

template real source · line 48 · raw

@-K:Data -> @+l:Nat -> @+d:Nat -> @+nl:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Node<K>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.NodeStore<K>