spec/containers/balanced_search_tree/main.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/spec/containers/balanced_search_tree/main.bend as Main

4 imports

import Base
import ../../lib/common.bend as C
import ../../../src/containers/balanced_search_tree.bend as M
import ../../lib/order.bend as SO

Types

type Model source · line 13 · raw

@-K:Data -> @-V:Data -> Data

TM

@-K:Data -> @-V:Data -> @limit:Nat -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Model<K, V>

type Cursor source · line 16 · raw

@-K:Data -> @-V:Data -> Data

CR

@-K:Data -> @-V:Data -> @map:Model<K, V> -> @next:Maybe<&2, K> -> @current:Maybe<&2, K> -> @lower:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @upper:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @forward:Bool -> Cursor<K, V>

type View source · line 19 · raw

@-K:Data -> @-V:Data -> Data

VW

@-K:Data -> @-V:Data -> @map:Model<K, V> -> @lower:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @upper:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @descending:Bool -> View<K, V>

type InvalidView source · line 22 · raw

@-K:Data -> @-V:Data -> Data

IV

@-K:Data -> @-V:Data -> @map:Model<K, V> -> @error:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Error -> InvalidView<K, V>

Definitions

def pick source · line 25 · raw

@-T:Type -> @+b:Bool -> @x:T -> @y:T -> T

def new source · line 32 · raw

@-K:Data -> @-V:Data -> Model<K, V>

def with_limit source · line 35 · raw

@-K:Data -> @-V:Data -> @+k:Nat -> Model<K, V>

def key source · line 38 · raw

@-K:Data -> @-V:Data -> @e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> K

def val source · line 43 · raw

@-K:Data -> @-V:Data -> @e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> V

def keys source · line 48 · raw

@-K:Data -> @-V:Data -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> List<&2, K>

def is_eq source · line 55 · raw

@c:Cmp -> Bool

def val_m source · line 72 · raw

@-K:Data -> @-V:Data -> @m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Maybe<&2, V>

def key_m source · line 79 · raw

@-K:Data -> @-V:Data -> @m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Maybe<&2, K>

def is_some source · line 89 · raw

@-X:Data -> @m:Maybe<&2, X> -> Bool

def ordering_ok source · line 124 · raw

@c:Cmp -> @inclusive:Bool -> Bool

def head source · line 202 · raw

@-X:Data -> @xs:List<&2, X> -> Maybe<&2, X>

def last source · line 209 · raw

@-X:Data -> @xs:List<&2, X> -> Maybe<&2, X>

def size source · line 239 · raw

@-K:Data -> @-V:Data -> @m:Model<K, V> -> Pair(Model<K, V>, Nat)

def is_empty source · line 244 · raw

@-K:Data -> @-V:Data -> @m:Model<K, V> -> Pair(Model<K, V>, Bool)

def or_default source · line 282 · raw

@-V:Data -> @m:Maybe<&2, V> -> @fallback:V -> V

def clear source · line 352 · raw

@-K:Data -> @-V:Data -> @m:Model<K, V> -> Model<K, V>

def first_entry source · line 357 · raw

@-K:Data -> @-V:Data -> @m:Model<K, V> -> Pair(Model<K, V>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>)

def last_entry source · line 362 · raw

@-K:Data -> @-V:Data -> @m:Model<K, V> -> Pair(Model<K, V>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>)

def first_key source · line 367 · raw

@-K:Data -> @-V:Data -> @m:Model<K, V> -> Pair(Model<K, V>, Maybe<&2, K>)

def last_key source · line 372 · raw

@-K:Data -> @-V:Data -> @m:Model<K, V> -> Pair(Model<K, V>, Maybe<&2, K>)

def poll_first_entry source · line 388 · raw

@-K:Data -> @-V:Data -> @m:Model<K, V> -> Pair(Model<K, V>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>)

def poll_last_entry source · line 397 · raw

@-K:Data -> @-V:Data -> @m:Model<K, V> -> Pair(Model<K, V>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>)

def iterator source · line 405 · raw

@-K:Data -> @-V:Data -> @m:Model<K, V> -> Cursor<K, V>

def descending_iterator source · line 410 · raw

@-K:Data -> @-V:Data -> @m:Model<K, V> -> Cursor<K, V>

def iterator_finish source · line 465 · raw

@-K:Data -> @-V:Data -> @c:Cursor<K, V> -> Model<K, V>

def key_result source · line 470 · raw

@-K:Data -> @-V:Data -> @r:Pair(Cursor<K, V>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>) -> Pair(Cursor<K, V>, Maybe<&2, K>)

def value_result source · line 475 · raw

@-K:Data -> @-V:Data -> @r:Pair(Cursor<K, V>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>) -> Pair(Cursor<K, V>, Maybe<&2, V>)

def view_checked source · line 489 · raw

@-K:Data -> @-V:Data -> @m:Model<K, V> -> @lo:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @hi:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @valid:Bool -> Result<&1, &1, InvalidView<K, V>, View<K, V>>

def head_map source · line 499 · raw

@-K:Data -> @-V:Data -> @m:Model<K, V> -> @hi:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> View<K, V>

def tail_map source · line 502 · raw

@-K:Data -> @-V:Data -> @m:Model<K, V> -> @lo:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> View<K, V>

def descending_map source · line 505 · raw

@-K:Data -> @-V:Data -> @m:Model<K, V> -> View<K, V>

def view_reverse source · line 508 · raw

@-K:Data -> @-V:Data -> @w:View<K, V> -> View<K, V>

def view_finish source · line 513 · raw

@-K:Data -> @-V:Data -> @w:View<K, V> -> Model<K, V>

def contained source · line 523 · raw

@-K:Data -> @-V:Data -> @r:Pair(View<K, V>, Maybe<&2, V>) -> Pair(View<K, V>, Bool)

def rewrap_put source · line 531 · raw

@-K:Data -> @-V:Data -> @lo:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @hi:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+d:Bool -> @r:Pair(Model<K, V>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected<K, V>, Maybe<&2, V>>) -> Pair(View<K, V>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected<K, V>, Maybe<&2, V>>)

def rewrap_val source · line 548 · raw

@-K:Data -> @-V:Data -> @lo:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @hi:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+d:Bool -> @r:Pair(Model<K, V>, Maybe<&2, V>) -> Pair(View<K, V>, Maybe<&2, V>)

def Empty_Map.new_empty source · line 684 · raw

@-K:Data -> @-V:Data -> Type

Empty_Map (101)

def Length.size_value source · line 688 · raw

@-K:Data -> @-V:Data -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Type

Length (114), Is_Empty (425)

def Length.is_empty_value source · line 692 · raw

@-K:Data -> @-V:Data -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Type

Length (114), Is_Empty (425)

def Clear.clear_empty source · line 696 · raw

@-K:Data -> @-V:Data -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Type

Clear (433)

def First.first_value source · line 756 · raw

@-K:Data -> @-V:Data -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Type

First/First_Element/First_Key (1116-1137)

def Last.last_value source · line 760 · raw

@-K:Data -> @-V:Data -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Type

Last/Last_Element/Last_Key (1148-1171)

Templates

template find_e source · line 65 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>

the first entry whose key is equal to k

template find source · line 86 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Maybe<&2, V>

template ins source · line 99 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+v:V -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>

k, absent, inserted before the first entry with a greater key

template set_val source · line 107 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+v:V -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>

the value of the first entry equal to k replaced (its key is kept)

template del source · line 115 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>

the first entry equal to k removed

template above_lower source · line 133 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> Bool

template below_upper source · line 142 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> Bool

template in_range source · line 151 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @lo:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @hi:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> Bool

template bounds_valid source · line 155 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @lo:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @hi:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> Bool

a view's bounds are valid when neither is past the other

template within source · line 170 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lo:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+hi:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>

template outside source · line 177 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lo:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+hi:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>

template first_where source · line 187 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+inclusive:Bool -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>

the first entry e with keep(cmp(k, e.key))

template last_where source · line 195 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+inclusive:Bool -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+best:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>

the last entry e below k (or equal, when inclusive)

template nav source · line 213 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+up:Bool -> @+inclusive:Bool -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>

ceiling (higher: strict) when up, floor (lower: strict) otherwise

template succ source · line 221 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+forward:Bool -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Maybe<&2, K>

the key after (forward) or before k

template start source · line 225 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+forward:Bool -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Maybe<&2, K>

the first entry past a bound, in a direction

template put_new source · line 249 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> Pair(Model<K, V>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected<K, V>, Maybe<&2, V>>)

template put_at source · line 252 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> @old:Maybe<&2, V> -> Pair(Model<K, V>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected<K, V>, Maybe<&2, V>>)

template put source · line 260 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:Model<K, V> -> @+k:K -> @+v:V -> Pair(Model<K, V>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected<K, V>, Maybe<&2, V>>)

k mapped to v: replaced when present, inserted when there is room

template absent_at source · line 265 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> @old:Maybe<&2, V> -> Pair(Model<K, V>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected<K, V>, Maybe<&2, V>>)

template put_if_absent source · line 272 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:Model<K, V> -> @+k:K -> @+v:V -> Pair(Model<K, V>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected<K, V>, Maybe<&2, V>>)

template get source · line 277 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:Model<K, V> -> @+k:K -> Pair(Model<K, V>, Maybe<&2, V>)

template get_or_default source · line 289 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:Model<K, V> -> @+k:K -> @fallback:V -> Pair(Model<K, V>, V)

template contains_key source · line 294 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:Model<K, V> -> @+k:K -> Pair(Model<K, V>, Bool)

template remove source · line 299 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:Model<K, V> -> @+k:K -> Pair(Model<K, V>, Maybe<&2, V>)

template replace_at source · line 304 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> @old:Maybe<&2, V> -> Pair(Model<K, V>, Maybe<&2, V>)

template replace source · line 311 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:Model<K, V> -> @+k:K -> @+v:V -> Pair(Model<K, V>, Maybe<&2, V>)

template any_value source · line 316 · raw

@-K:Data -> @-V:Data -> @-eq:(@_:V -> @_:V -> Bool) -> @+w:V -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Bool

template contains_value source · line 323 · raw

@-K:Data -> @-V:Data -> @-eq:(@_:V -> @_:V -> Bool) -> @m:Model<K, V> -> @+w:V -> Pair(Model<K, V>, Bool)

template remove_if_at source · line 328 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-eq:(@_:V -> @_:V -> Bool) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+expected:V -> @old:Maybe<&2, V> -> Pair(Model<K, V>, Bool)

template remove_if_equal source · line 335 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-eq:(@_:V -> @_:V -> Bool) -> @m:Model<K, V> -> @+k:K -> @+expected:V -> Pair(Model<K, V>, Bool)

template replace_if_at source · line 340 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-eq:(@_:V -> @_:V -> Bool) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+expected:V -> @+replacement:V -> @old:Maybe<&2, V> -> Pair(Model<K, V>, Bool)

template replace_if_equal source · line 347 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-eq:(@_:V -> @_:V -> Bool) -> @m:Model<K, V> -> @+k:K -> @+expected:V -> @+replacement:V -> Pair(Model<K, V>, Bool)

template nav_entry source · line 378 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:Model<K, V> -> @+k:K -> @+up:Bool -> @+inclusive:Bool -> Pair(Model<K, V>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>)

lower/floor (up False) and ceiling/higher (up True) entries

template nav_key source · line 383 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:Model<K, V> -> @+k:K -> @+up:Bool -> @+inclusive:Bool -> Pair(Model<K, V>, Maybe<&2, K>)

template next_at source · line 415 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+current:Maybe<&2, K> -> @+lo:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+hi:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+forward:Bool -> @found:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Pair(Cursor<K, V>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>)

template iterator_next source · line 422 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @c:Cursor<K, V> -> Pair(Cursor<K, V>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>)

template iterator_has_next source · line 431 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @c:Cursor<K, V> -> Pair(Cursor<K, V>, Bool)

template set_value_at source · line 440 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @next:Maybe<&2, K> -> @+k:K -> @lo:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @hi:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+forward:Bool -> @+v:V -> @old:Maybe<&2, V> -> Pair(Cursor<K, V>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Error, V>)

template iterator_set_value source · line 447 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @c:Cursor<K, V> -> @+v:V -> Pair(Cursor<K, V>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Error, V>)

template iterator_remove source · line 456 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @c:Cursor<K, V> -> Pair(Cursor<K, V>, Maybe<&2, V>)

template iterator_next_key source · line 480 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @c:Cursor<K, V> -> Pair(Cursor<K, V>, Maybe<&2, K>)

template iterator_next_value source · line 483 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @c:Cursor<K, V> -> Pair(Cursor<K, V>, Maybe<&2, V>)

template sub_map source · line 496 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:Model<K, V> -> @+lo:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+hi:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> Result<&1, &1, InvalidView<K, V>, View<K, V>>

template view_get source · line 518 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @w:View<K, V> -> @+k:K -> Pair(View<K, V>, Maybe<&2, V>)

template view_contains_key source · line 528 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @w:View<K, V> -> @+k:K -> Pair(View<K, V>, Bool)

template view_put_at source · line 536 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:Model<K, V> -> @+k:K -> @+v:V -> @lo:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @hi:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+d:Bool -> @valid:Bool -> Pair(View<K, V>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected<K, V>, Maybe<&2, V>>)

template view_put source · line 543 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @w:View<K, V> -> @+k:K -> @+v:V -> Pair(View<K, V>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Rejected<K, V>, Maybe<&2, V>>)

template view_remove_at source · line 553 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:Model<K, V> -> @+k:K -> @lo:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @hi:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Bound<K> -> @+d:Bool -> @valid:Bool -> Pair(View<K, V>, Maybe<&2, V>)

template view_remove source · line 560 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @w:View<K, V> -> @+k:K -> Pair(View<K, V>, Maybe<&2, V>)

template view_size source · line 565 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @w:View<K, V> -> Pair(View<K, V>, Nat)

template view_clear source · line 570 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @w:View<K, V> -> View<K, V>

template view_extreme source · line 576 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @w:View<K, V> -> @+first:Bool -> Pair(View<K, V>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>)

the view's first (or last) entry in its own direction

template view_first_entry source · line 581 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @w:View<K, V> -> Pair(View<K, V>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>)

template view_last_entry source · line 584 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @w:View<K, V> -> Pair(View<K, V>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>)

template view_nav source · line 589 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @w:View<K, V> -> @+k:K -> @+higher:Bool -> @+inclusive:Bool -> Pair(View<K, V>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>)

the view's lower/floor (higher False) or ceiling/higher (higher True) entry, in the view's own direction

template view_iterator source · line 594 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @w:View<K, V> -> Cursor<K, V>

template ordered source · line 601 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Bool

the map's invariant: consecutive keys strictly increasing (SPARK's ordered maps keep Keys (Container) sorted; Formal_Ordered_Maps, Formal_Model.K)

template Include.find_ins_other source · line 652 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+v:V -> @+q:K -> @+hq:{is_eq(cmp(q, k)) == False{} : Bool} -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Type

Include (754)

template Include.ins_length source · line 656 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+v:V -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Type

Include (754)

template Replace.find_set_same source · line 660 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+v:V -> @+e0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hp:{find_e(K, V, cmp, k, es) == Some{e0} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> Type

Replace (846)

template Include.find_set_other source · line 664 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(K, cmp) -> @+k:K -> @+v:V -> @+q:K -> @+hq:{is_eq(cmp(q, k)) == False{} : Bool} -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Type

Include (754)

template Include.set_length source · line 668 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+v:V -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Type

Include (754)

template Exclude.find_del_other source · line 672 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(K, cmp) -> @+k:K -> @+q:K -> @+hq:{is_eq(cmp(q, k)) == False{} : Bool} -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> Type

Exclude (884) / Delete (937)

template Exclude.find_del_same source · line 676 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(K, cmp) -> @+k:K -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hord:{ordered(K, V, cmp, es) == True{} : Bool} -> Type

Exclude (884) / Delete (937)

template Exclude.del_length source · line 680 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+e0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+hp:{find_e(K, V, cmp, k, es) == Some{e0} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> Type

Exclude (884) / Delete (937)

template Element.get_value source · line 700 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> Type

Element (Key) (1283), Find (1257)

template Element.get_or_default_value source · line 704 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+d:V -> Type

Element (Key) (1283), Find (1257)

template Contains.contains_value source · line 708 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> Type

Contains (1332)

template Include.put_present source · line 712 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> @+e0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+hp:{find_e(K, V, cmp, k, es) == Some{e0} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> Type

Include (754)

template Include.put_absent source · line 716 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> @+ha:{find_e(K, V, cmp, k, es) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> @+hr:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, es), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(l)) == True{} : Bool} -> Type

Include (754)

template Include.put_full source · line 720 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> @+ha:{find_e(K, V, cmp, k, es) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> @+hr:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, es), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(l)) == False{} : Bool} -> Type

Include (754)

template Include.put_found_present source · line 724 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> @+e0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+hp:{find_e(K, V, cmp, k, es) == Some{e0} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> Type

Include (754)

template Include.put_found_absent source · line 728 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/order.Order(K, cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> @+ha:{find_e(K, V, cmp, k, es) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> Type

Include (754)

template Insert.put_if_absent_present source · line 732 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> @+e0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+hp:{find_e(K, V, cmp, k, es) == Some{e0} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> Type

Insert (612/697, keeps a present key) put_if_absent

template Insert.put_if_absent_absent source · line 736 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> @+ha:{find_e(K, V, cmp, k, es) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> @+hr:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>, es), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(l)) == True{} : Bool} -> Type

Insert (612/697, keeps a present key) put_if_absent

template Replace.replace_present source · line 740 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> @+e0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+hp:{find_e(K, V, cmp, k, es) == Some{e0} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> Type

Replace (846)

template Replace.replace_absent source · line 744 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+v:V -> @+ha:{find_e(K, V, cmp, k, es) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> Type

Replace (846)

template Exclude.remove_present source · line 748 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+e0:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V> -> @+hp:{find_e(K, V, cmp, k, es) == Some{e0} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> Type

Exclude (884) / Delete (937)

template Exclude.remove_absent source · line 752 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+ha:{find_e(K, V, cmp, k, es) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>>} -> Type

Exclude (884) / Delete (937)

template Floor.nav_value source · line 764 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+l:Nat -> @+es:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/balanced_search_tree.Entry<K, V>> -> @+k:K -> @+up:Bool -> @+inclusive:Bool -> Type

Floor (1291), Ceiling (1312)