src/containers/balanced_search_tree.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as Balanced_search_tree

Generated by tools/generators/tree_map.py; edit algorithm definitions there.

3 imports

import Base
import ./dynamic_array.bend as D
import ./types/dynamic_array.bend as DE

Types

type Node source · line 9 · raw

@-K:Data -> Data

Indexed CLRS red-black map. Keys and payloads are Data for this version. Comparator is a type index: changing comparator requires rebuilding a map. Node links are slot indices plus one; zero is the black NIL sentinel.

Free
```
@-K:Data -> @next:Nat -> Node<K>
```

N

@-K:Data -> @red:Bool -> @left:Nat -> @right:Nat -> @parent:Nat -> @key:K -> Node<K>

type NodeStore source · line 22 · raw

@-K:Data -> Type

Node storage: one array per node field instead of one array of Node records. Reading a record out of an array hands back a shared copy that the runtime reference-counts and takes apart field by field; a field read out of its own array is a plain word. The store has the shape of a dynamic array of nodes: slots [0, used) are live, the capacity is 2^depth <= 2^limit, and it grows by doubling. A slot holds the encoding of its node by ntag (0 free, 1 black, 2 red), nleft (the free-list link of a free slot), nright, nparent and nkey (None when free); every other slot holds the encoding of Free{0}, so each array is exactly its field of the node list, padded.

NS

@-K:Data -> @limit:Nat -> @depth:Nat -> @cap:Nat -> @used:Nat -> @tags:Array<Nat> -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> NodeStore<K>

type TreeMap source · line 25 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> Type

TM

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @size:Nat -> @root:Nat -> @first:Nat -> @last:Nat -> @free:Nat -> @nodes:NodeStore<K> -> @payloads:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>> -> TreeMap<K, V, cmp>

type Entry source · line 29 · raw

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

Entry

@-K:Data -> @-V:Data -> @key:K -> @value:V -> Entry<K, V>

type Error source · line 32 · raw

Data

CapacityExceeded
```
Error
```
OutOfRange
```
Error
```
NoCurrent
```
Error
```
InvalidBounds
```
Error
```

type Rejected source · line 38 · raw

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

Rejected

@-K:Data -> @-V:Data -> @error:Error -> @key:K -> @value:V -> Rejected<K, V>

type Search source · line 41 · raw

Data

Search

@found:Nat -> @parent:Nat -> @left:Bool -> Search

type Fix source · line 44 · raw

Data

Fix
```
@node:Nat -> @more:Bool -> Fix
```

type Ascend source · line 47 · raw

Data

Ascend

@child:Nat -> @parent:Nat -> @done:Bool -> Ascend

type DeleteFix source · line 52 · raw

Data

A direct branch preserves scalar traversal state in native code. Passing these records through pick(-T: Type) erases their layout and boxes both arms.

DF

@node:Nat -> @parent:Nat -> @more:Bool -> DeleteFix

type NavEnd source · line 55 · raw

Data

NavBest
```
@id:Nat -> NavEnd
```
NavEqual
```
@id:Nat -> NavEnd
```

type Bound source · line 59 · raw

@-K:Data -> Data

Unbounded
```
@-K:Data -> Bound<K>
```
Inclusive
```
@-K:Data -> @key:K -> Bound<K>
```
Exclusive
```
@-K:Data -> @key:K -> Bound<K>
```

type View source · line 64 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> Type

View

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @map:TreeMap<K, V, cmp> -> @lower:Bound<K> -> @upper:Bound<K> -> @descending:Bool -> View<K, V, cmp>

type InvalidView source · line 67 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> Type

InvalidView

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @map:TreeMap<K, V, cmp> -> @error:Error -> InvalidView<K, V, cmp>

type Cursor source · line 70 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> Type

Cursor

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @map:TreeMap<K, V, cmp> -> @next:Nat -> @current:Nat -> @lower:Bound<K> -> @upper:Bound<K> -> @forward:Bool -> Cursor<K, V, cmp>

Definitions

def ns_nats source · line 122 · raw

@+d:Nat -> Array<Nat>

def ns_red_tag source · line 154 · raw

@red:Bool -> Nat

def pick source · line 182 · raw

@-T:Type -> @b:Bool -> @yes:T -> @no:T -> T

def ascend_choice source · line 307 · raw

@x:Nat -> @p:Nat -> @q:Nat -> @found:Bool -> Ascend

def ordering_ok source · line 355 · raw

@order:Cmp -> @inclusive:Bool -> Bool

def ns_grow_nats source · line 531 · raw

@+depth:Nat -> @a:Array<Nat> -> Array<Nat>

Templates

template ntag source · line 74 · raw

@-K:Data -> @n:Node<K> -> Nat

template nleft source · line 85 · raw

@-K:Data -> @n:Node<K> -> Nat

template nright source · line 92 · raw

@-K:Data -> @n:Node<K> -> Nat

template nparent source · line 99 · raw

@-K:Data -> @n:Node<K> -> Nat

template nkey source · line 106 · raw

@-K:Data -> @n:Node<K> -> Maybe<&2, K>

template mk_node source · line 113 · raw

@-K:Data -> @+t:Nat -> @+l:Nat -> @+r:Nat -> @+p:Nat -> @k:Maybe<&2, K> -> Node<K>

template ns_nokeys source · line 125 · raw

@-K:Data -> @+d:Nat -> Array<Maybe<&2, K>>

template ns_length source · line 128 · raw

@-K:Data -> @s:NodeStore<K> -> Pair(NodeStore<K>, Nat)

template ns_tag_fin source · line 134 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @q:Pair(Array<Nat>, Nat) -> Pair(NodeStore<K>, Nat)

template ns_left_fin source · line 138 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @tags:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @q:Pair(Array<Nat>, Nat) -> Pair(NodeStore<K>, Nat)

template ns_right_fin source · line 142 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @tags:Array<Nat> -> @lefts:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @q:Pair(Array<Nat>, Nat) -> Pair(NodeStore<K>, Nat)

template ns_parent_fin source · line 146 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @tags:Array<Nat> -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @q:Pair(Array<Nat>, Nat) -> Pair(NodeStore<K>, Nat)

template ns_key_fin source · line 150 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @tags:Array<Nat> -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @q:Pair(Array<Maybe<&2, K>>, Maybe<&2, K>) -> Pair(NodeStore<K>, Maybe<&2, K>)

template ns_set_left_tag source · line 161 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @+i:Nat -> @+v:Nat -> @q:Pair(Array<Nat>, Nat) -> NodeStore<K>

template ns_set_right_tag source · line 168 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @+i:Nat -> @+v:Nat -> @q:Pair(Array<Nat>, Nat) -> NodeStore<K>

template ns_set_parent_tag source · line 175 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @+i:Nat -> @+v:Nat -> @q:Pair(Array<Nat>, Nat) -> NodeStore<K>

template node_red source · line 189 · raw

@-K:Data -> @n:Node<K> -> Bool

template node_left source · line 196 · raw

@-K:Data -> @n:Node<K> -> Nat

template node_right source · line 203 · raw

@-K:Data -> @n:Node<K> -> Nat

template node_parent source · line 210 · raw

@-K:Data -> @n:Node<K> -> Nat

template node_key source · line 217 · raw

@-K:Data -> @n:Node<K> -> Maybe<&2, K>

template size source · line 224 · raw

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

template root_id source · line 228 · raw

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

template first_id source · line 232 · raw

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

template last_id source · line 236 · raw

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

template read_finish source · line 240 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @payloads:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>> -> @r:Pair(NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Node<K>>) -> Pair(TreeMap<K, V, cmp>, Node<K>)

template write_finish source · line 247 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @payloads:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>> -> @r:Pair(NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>) -> TreeMap<K, V, cmp>

template set_root source · line 251 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+root:Nat -> TreeMap<K, V, cmp>

template probe_node source · line 255 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+id:Nat -> @+k:K -> @r:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, Pair(Node<K>, Cmp))

template search_key source · line 262 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+id:Nat -> @+k:K -> @r:Pair(NodeStore<K>, Maybe<&2, K>) -> Pair(NodeStore<K>, Pair(Nat, Maybe<&2, Cmp>))

template search_fin source · line 269 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @payloads:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>> -> @r:Pair(NodeStore<K>, Search) -> Pair(TreeMap<K, V, cmp>, Search)

template exchange_finish source · line 273 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @nodes:NodeStore<K> -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Maybe<&2, V>>) -> Pair(TreeMap<K, V, cmp>, Maybe<&2, V>)

template append_rollback source · line 280 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @payloads:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>> -> @+k:K -> @+v:V -> @r:Pair(NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Node<K>>) -> Pair(TreeMap<K, V, cmp>, Result<&2, &2, Rejected<K, V>, Nat>)

template free_header source · line 284 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+free:Nat -> TreeMap<K, V, cmp>

template reuse_slot_1 source · line 288 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+id:Nat -> @pair_result:Pair(TreeMap<K, V, cmp>, Maybe<&2, V>) -> Pair(TreeMap<K, V, cmp>, Result<&2, &2, Rejected<K, V>, Nat>)

template put_replaced source · line 292 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @r:Pair(TreeMap<K, V, cmp>, Maybe<&2, V>) -> Pair(TreeMap<K, V, cmp>, Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>)

template get_id_finish source · line 296 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @nodes:NodeStore<K> -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Maybe<&2, V>>) -> Pair(TreeMap<K, V, cmp>, Maybe<&2, V>)

template contains_found source · line 303 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @r:Pair(TreeMap<K, V, cmp>, Search) -> Pair(TreeMap<K, V, cmp>, Bool)

template neighbor_slots_finish source · line 314 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @payloads:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>> -> @r:Pair(NodeStore<K>, Nat) -> Pair(TreeMap<K, V, cmp>, Nat)

template move_successor_3 source · line 318 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+source:Nat -> @pair_result:Pair(TreeMap<K, V, cmp>, Maybe<&2, V>) -> Pair(TreeMap<K, V, cmp>, Nat)

template release_header source · line 322 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id:Nat -> TreeMap<K, V, cmp>

template set_ends source · line 326 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+lo:Nat -> @+hi:Nat -> TreeMap<K, V, cmp>

template is_empty_1 source · line 330 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @pair_result:Pair(TreeMap<K, V, cmp>, Nat) -> Pair(TreeMap<K, V, cmp>, Bool)

template entry_value source · line 334 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @k:Maybe<&2, K> -> @r:Pair(TreeMap<K, V, cmp>, Maybe<&2, V>) -> Pair(TreeMap<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template snap_kv source · line 341 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @payloads:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>> -> @nodes:NodeStore<K> -> @mk:Maybe<&2, K> -> @mv:Maybe<&2, V> -> Pair(TreeMap<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template default_value source · line 348 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+fallback:V -> @r:Pair(TreeMap<K, V, cmp>, Maybe<&2, V>) -> Pair(TreeMap<K, V, cmp>, V)

template view_checked source · line 364 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @lower:Bound<K> -> @upper:Bound<K> -> @+descending:Bool -> @+valid:Bool -> Result<&1, &1, InvalidView<K, V, cmp>, View<K, V, cmp>>

template head_map source · line 371 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @upper:Bound<K> -> View<K, V, cmp>

template tail_map source · line 374 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @lower:Bound<K> -> View<K, V, cmp>

template descending_map source · line 377 · raw

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

template view_reverse source · line 380 · raw

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

template view_finish source · line 384 · raw

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

template view_value source · line 388 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @lower:Bound<K> -> @upper:Bound<K> -> @+descending:Bool -> @r:Pair(TreeMap<K, V, cmp>, Maybe<&2, V>) -> Pair(View<K, V, cmp>, Maybe<&2, V>)

template view_put_finish source · line 392 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @lower:Bound<K> -> @upper:Bound<K> -> @+descending:Bool -> @r:Pair(TreeMap<K, V, cmp>, Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>) -> Pair(View<K, V, cmp>, Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>)

template cursor_started source · line 396 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @lower:Bound<K> -> @upper:Bound<K> -> @+forward:Bool -> @r:Pair(TreeMap<K, V, cmp>, Nat) -> Cursor<K, V, cmp>

template iterator_finish source · line 400 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @cursor:Cursor<K, V, cmp> -> TreeMap<K, V, cmp>

template iterator_view source · line 404 · raw

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

template iterator_yield source · line 408 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+id:Nat -> @lower:Bound<K> -> @upper:Bound<K> -> @+forward:Bool -> @entry:Entry<K, V> -> @r:Pair(TreeMap<K, V, cmp>, Nat) -> Pair(Cursor<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template iterator_set_done source · line 412 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+next:Nat -> @+current:Nat -> @lower:Bound<K> -> @upper:Bound<K> -> @+forward:Bool -> @r:Pair(TreeMap<K, V, cmp>, Maybe<&2, V>) -> Pair(Cursor<K, V, cmp>, Result<&2, &2, Error, V>)

template iterator_relocated source · line 419 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @lower:Bound<K> -> @upper:Bound<K> -> @+forward:Bool -> @removed:Maybe<&2, V> -> @r:Pair(TreeMap<K, V, cmp>, Search) -> Pair(Cursor<K, V, cmp>, Maybe<&2, V>)

template iterator_key_result source · line 423 · raw

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

template iterator_value_result source · line 430 · raw

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

template changed_value source · line 437 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @r:Pair(TreeMap<K, V, cmp>, Maybe<&2, V>) -> Pair(TreeMap<K, V, cmp>, Bool)

template view_contains_value source · line 444 · raw

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

template view_entry_checked source · line 451 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @lower:Bound<K> -> @upper:Bound<K> -> @+descending:Bool -> @entry:Entry<K, V> -> @+valid:Bool -> Pair(View<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template ns_empty source · line 458 · raw

@-K:Data -> @+limit:Nat -> NodeStore<K>

template ns_rk source · line 461 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @tags:Array<Nat> -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @+t:Nat -> @+l:Nat -> @+r:Nat -> @+p:Nat -> @q:Pair(Array<Maybe<&2, K>>, Maybe<&2, K>) -> Pair(NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Node<K>>)

template ns_tag_ok source · line 465 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @tags:Array<Nat> -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @+i:Nat -> @ok:Bool -> Pair(NodeStore<K>, Nat)

template ns_left_ok source · line 472 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @tags:Array<Nat> -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @+i:Nat -> @ok:Bool -> Pair(NodeStore<K>, Nat)

template ns_right_ok source · line 479 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @tags:Array<Nat> -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @+i:Nat -> @ok:Bool -> Pair(NodeStore<K>, Nat)

template ns_parent_ok source · line 486 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @tags:Array<Nat> -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @+i:Nat -> @ok:Bool -> Pair(NodeStore<K>, Nat)

template ns_key_ok source · line 493 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @tags:Array<Nat> -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @+i:Nat -> @ok:Bool -> Pair(NodeStore<K>, Maybe<&2, K>)

template ns_set_left_ok source · line 500 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @tags:Array<Nat> -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @+i:Nat -> @+v:Nat -> @ok:Bool -> NodeStore<K>

template ns_set_right_ok source · line 507 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @tags:Array<Nat> -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @+i:Nat -> @+v:Nat -> @ok:Bool -> NodeStore<K>

template ns_set_parent_ok source · line 514 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @tags:Array<Nat> -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @+i:Nat -> @+v:Nat -> @ok:Bool -> NodeStore<K>

template ns_set_red_tag source · line 521 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @+i:Nat -> @+v:Bool -> @q:Pair(Array<Nat>, Nat) -> NodeStore<K>

template ns_put source · line 528 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @tags:Array<Nat> -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @+i:U32 -> @+node:Node<K> -> NodeStore<K>

template ns_grow_keys source · line 534 · raw

@-K:Data -> @+depth:Nat -> @a:Array<Maybe<&2, K>> -> Array<Maybe<&2, K>>

template child source · line 537 · raw

@-K:Data -> @+n:Node<K> -> @forward:Bool -> Nat

template exchange source · line 542 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id:Nat -> @value:Maybe<&2, V> -> Pair(TreeMap<K, V, cmp>, Maybe<&2, V>)

template insert_header source · line 549 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id:Nat -> @+p:Nat -> @+on_left:Bool -> TreeMap<K, V, cmp>

template get_id source · line 553 · raw

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

template ascend_step_node source · line 560 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+x:Nat -> @+p:Nat -> @+forward:Bool -> @r:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, Ascend)

template ascend_par source · line 567 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+x:Nat -> @+p:Nat -> @+s:Nat -> @r:Pair(NodeStore<K>, Nat) -> Pair(NodeStore<K>, Ascend)

template refresh_ends_3 source · line 571 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lo:Nat -> @pair_result:Pair(TreeMap<K, V, cmp>, Nat) -> TreeMap<K, V, cmp>

template is_empty source · line 575 · raw

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

template key_finish source · line 578 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @r:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, Maybe<&2, K>)

template snap_key source · line 582 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @payloads:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>> -> @mv:Maybe<&2, V> -> @r:Pair(NodeStore<K>, Maybe<&2, K>) -> Pair(TreeMap<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template above_lower source · line 586 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @bound:Bound<K> -> Bool

template below_upper source · line 595 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @bound:Bound<K> -> Bool

template bounds_valid source · line 604 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @lower:Bound<K> -> @upper:Bound<K> -> Bool

template range_unbounded source · line 619 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+forward:Bool -> Pair(TreeMap<K, V, cmp>, Nat)

template iterator source · line 626 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> Cursor<K, V, cmp>

template descending_iterator source · line 629 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> Cursor<K, V, cmp>

template ns_new source · line 632 · raw

@-K:Data -> NodeStore<K>

template ns_with_limit source · line 635 · raw

@-K:Data -> @+k:Nat -> NodeStore<K>

template ns_rp source · line 638 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @tags:Array<Nat> -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @+i:U32 -> @+t:Nat -> @+l:Nat -> @+r:Nat -> @q:Pair(Array<Nat>, Nat) -> Pair(NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Node<K>>)

template ns_tag_at source · line 642 · raw

@-K:Data -> @s:NodeStore<K> -> @+i:Nat -> Pair(NodeStore<K>, Nat)

template ns_left_at source · line 646 · raw

@-K:Data -> @s:NodeStore<K> -> @+i:Nat -> Pair(NodeStore<K>, Nat)

template ns_right_at source · line 650 · raw

@-K:Data -> @s:NodeStore<K> -> @+i:Nat -> Pair(NodeStore<K>, Nat)

template ns_parent_at source · line 654 · raw

@-K:Data -> @s:NodeStore<K> -> @+i:Nat -> Pair(NodeStore<K>, Nat)

template ns_key_at source · line 658 · raw

@-K:Data -> @s:NodeStore<K> -> @+i:Nat -> Pair(NodeStore<K>, Maybe<&2, K>)

template ns_set_left source · line 664 · raw

@-K:Data -> @s:NodeStore<K> -> @+i:Nat -> @+v:Nat -> NodeStore<K>

template ns_set_right source · line 668 · raw

@-K:Data -> @s:NodeStore<K> -> @+i:Nat -> @+v:Nat -> NodeStore<K>

template ns_set_parent source · line 672 · raw

@-K:Data -> @s:NodeStore<K> -> @+i:Nat -> @+v:Nat -> NodeStore<K>

template ns_set_red_ok source · line 676 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @tags:Array<Nat> -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @+i:Nat -> @+v:Bool -> @ok:Bool -> NodeStore<K>

template ns_set_ok source · line 683 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @tags:Array<Nat> -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @+i:Nat -> @+node:Node<K> -> @ok:Bool -> Pair(NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

template ns_push_room source · line 690 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @tags:Array<Nat> -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @+node:Node<K> -> @room:Bool -> @grow:Bool -> Pair(NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

template ns_drop source · line 699 · raw

@-K:Data -> @s:NodeStore<K> -> @+m:Nat -> NodeStore<K>

template get_found source · line 703 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @r:Pair(TreeMap<K, V, cmp>, Search) -> Pair(TreeMap<K, V, cmp>, Maybe<&2, V>)

template replace_found source · line 707 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+v:V -> @r:Pair(TreeMap<K, V, cmp>, Search) -> Pair(TreeMap<K, V, cmp>, Maybe<&2, V>)

template in_range source · line 714 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @lower:Bound<K> -> @upper:Bound<K> -> Bool

template sub_map source · line 717 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+lower:Bound<K> -> @+upper:Bound<K> -> Result<&1, &1, InvalidView<K, V, cmp>, View<K, V, cmp>>

template iterator_set_value source · line 720 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @cursor:Cursor<K, V, cmp> -> @+v:V -> Pair(Cursor<K, V, cmp>, Result<&2, &2, Error, V>)

template entry_set source · line 727 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> Cursor<K, V, cmp>

template key_set source · line 730 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> Cursor<K, V, cmp>

template values source · line 733 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> Cursor<K, V, cmp>

template replace_if_apply source · line 736 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id:Nat -> @+replacement:V -> @+equal:Bool -> Pair(TreeMap<K, V, cmp>, Bool)

template ns_rr source · line 743 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @tags:Array<Nat> -> @lefts:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @+i:U32 -> @+t:Nat -> @+l:Nat -> @q:Pair(Array<Nat>, Nat) -> Pair(NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Node<K>>)

template ns_set_red source · line 747 · raw

@-K:Data -> @s:NodeStore<K> -> @+i:Nat -> @+v:Bool -> NodeStore<K>

template ns_set source · line 753 · raw

@-K:Data -> @s:NodeStore<K> -> @+i:Nat -> @+node:Node<K> -> Pair(NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

template ns_push source · line 759 · raw

@-K:Data -> @s:NodeStore<K> -> @+node:Node<K> -> Pair(NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

template ns_pop_fin source · line 765 · raw

@-K:Data -> @+m:Nat -> @r:Pair(NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Node<K>>) -> Pair(NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Node<K>>)

template ns_clear_go source · line 769 · raw

@-K:Data -> @k:Nat -> @s:NodeStore<K> -> NodeStore<K>

template new source · line 777 · raw

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

O(used): resets the live slots top down and keeps the capacity.

template set_left source · line 780 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id:Nat -> @+v:Nat -> TreeMap<K, V, cmp>

template set_right source · line 787 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id:Nat -> @+v:Nat -> TreeMap<K, V, cmp>

template set_parent source · line 794 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id:Nat -> @+v:Nat -> TreeMap<K, V, cmp>

template search_probe source · line 801 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @nodes:NodeStore<K> -> @+id:Nat -> @+k:K -> Pair(NodeStore<K>, Pair(Nat, Maybe<&2, Cmp>))

template side_at source · line 808 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @nodes:NodeStore<K> -> @+left:Bool -> @+i:Nat -> Pair(NodeStore<K>, Nat)

template ascend_side source · line 815 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+x:Nat -> @+p:Nat -> @+i:Nat -> @r:Pair(NodeStore<K>, Nat) -> Pair(NodeStore<K>, Ascend)

template snap_value source · line 819 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+i:Nat -> @r:Pair(TreeMap<K, V, cmp>, Maybe<&2, V>) -> Pair(TreeMap<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template with_limit source · line 823 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+limit:Nat -> TreeMap<K, V, cmp>

template replace_if_value source · line 826 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-eq:(@_:V -> @_:V -> Bool) -> @+id:Nat -> @+expected:V -> @+replacement:V -> @r:Pair(TreeMap<K, V, cmp>, Maybe<&2, V>) -> Pair(TreeMap<K, V, cmp>, Bool)

template iterator_has_checked source · line 833 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+next:Nat -> @+current:Nat -> @+lower:Bound<K> -> @+upper:Bound<K> -> @+forward:Bool -> @r:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(Cursor<K, V, cmp>, Bool)

template view_entry_result source · line 840 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+lower:Bound<K> -> @+upper:Bound<K> -> @+descending:Bool -> @r:Pair(TreeMap<K, V, cmp>, Maybe<&2, Entry<K, V>>) -> Pair(View<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template ns_rl source · line 847 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @tags:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @+i:U32 -> @+t:Nat -> @q:Pair(Array<Nat>, Nat) -> Pair(NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Node<K>>)

template ns_clear source · line 851 · raw

@-K:Data -> @s:NodeStore<K> -> NodeStore<K>

template write source · line 856 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id:Nat -> @+node:Node<K> -> TreeMap<K, V, cmp>

template set_red source · line 863 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id:Nat -> @+v:Bool -> TreeMap<K, V, cmp>

template attach_side source · line 870 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+p:Nat -> @+x:Nat -> @+on_left:Bool -> TreeMap<K, V, cmp>

template search_down2 source · line 879 · raw

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

template ascend_tag source · line 883 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+x:Nat -> @+p:Nat -> @+i:Nat -> @+forward:Bool -> @r:Pair(NodeStore<K>, Nat) -> Pair(NodeStore<K>, Ascend)

template extreme_tag source · line 890 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+forward:Bool -> @+i:Nat -> @r:Pair(NodeStore<K>, Nat) -> Pair(NodeStore<K>, Nat)

template snap_at source · line 897 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+id:Nat -> @m:TreeMap<K, V, cmp> -> Pair(TreeMap<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template replace_if_found source · line 904 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-eq:(@_:V -> @_:V -> Bool) -> @+expected:V -> @+replacement:V -> @r:Pair(TreeMap<K, V, cmp>, Search) -> Pair(TreeMap<K, V, cmp>, Bool)

template ns_rt source · line 908 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @+i:U32 -> @q:Pair(Array<Nat>, Nat) -> Pair(NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Node<K>>)

template attach source · line 912 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+p:Nat -> @+x:Nat -> @+on_left:Bool -> TreeMap<K, V, cmp>

template search_down source · line 915 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @nodes:NodeStore<K> -> @+id:Nat -> @+left:Bool -> @+k:K -> Pair(NodeStore<K>, Pair(Nat, Maybe<&2, Cmp>))

template black_root_1 source · line 922 · raw

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

template reuse_slot source · line 926 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id:Nat -> @+next:Nat -> @+p:Nat -> @+k:K -> @+v:V -> Pair(TreeMap<K, V, cmp>, Result<&2, &2, Rejected<K, V>, Nat>)

template ascend_at source · line 929 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+x:Nat -> @+p:Nat -> @+forward:Bool -> @nodes:NodeStore<K> -> Pair(NodeStore<K>, Ascend)

template extreme_at source · line 936 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+forward:Bool -> @nodes:NodeStore<K> -> @+i:Nat -> Pair(NodeStore<K>, Nat)

template set_key_node source · line 939 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id:Nat -> @+k:K -> @+node:Node<K> -> TreeMap<K, V, cmp>

template recycle source · line 946 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id:Nat -> TreeMap<K, V, cmp>

template clear source · line 950 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> TreeMap<K, V, cmp>

template entry_snapshot source · line 954 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @r:Pair(TreeMap<K, V, cmp>, Nat) -> Pair(TreeMap<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template ns_get_ok source · line 958 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @tags:Array<Nat> -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> @+i:Nat -> @ok:Bool -> Pair(NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Node<K>>)

template rotate_left_3 source · line 965 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+x:Nat -> @+xn:Node<K> -> @+yn:Node<K> -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> TreeMap<K, V, cmp>

template rotate_right_3 source · line 969 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+x:Nat -> @+xn:Node<K> -> @+yn:Node<K> -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> TreeMap<K, V, cmp>

template search_fast source · line 973 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+fuel:Nat -> @+k:K -> @+p:Nat -> @+on_left:Bool -> @st:Pair(NodeStore<K>, Pair(Nat, Maybe<&2, Cmp>)) -> Pair(NodeStore<K>, Search)

template black_root source · line 986 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> TreeMap<K, V, cmp>

template alloc_read source · line 990 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+id:Nat -> @+p:Nat -> @+k:K -> @+v:V -> @r:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, Result<&2, &2, Rejected<K, V>, Nat>)

template ascend_slots_loop source · line 997 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+fuel:Nat -> @+forward:Bool -> @st:Pair(NodeStore<K>, Ascend) -> Pair(NodeStore<K>, Nat)

template extreme_slots_loop source · line 1006 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+fuel:Nat -> @+forward:Bool -> @+id:Nat -> @st:Pair(NodeStore<K>, Nat) -> Pair(NodeStore<K>, Nat)

template set_key_1 source · line 1015 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+id:Nat -> @+k:K -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> TreeMap<K, V, cmp>

template nav_fast source · line 1019 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+fuel:Nat -> @+k:K -> @+higher:Bool -> @+best:Nat -> @st:Pair(NodeStore<K>, Pair(Nat, Maybe<&2, Cmp>)) -> Pair(NodeStore<K>, NavEnd)

template first_entry source · line 1032 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> Pair(TreeMap<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template last_entry source · line 1035 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> Pair(TreeMap<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template ns_get source · line 1038 · raw

@-K:Data -> @s:NodeStore<K> -> @+i:Nat -> Pair(NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Node<K>>)

template search source · line 1044 · raw

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

template neighbor_slots source · line 1048 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @nodes:NodeStore<K> -> @+n:Nat -> @+id:Nat -> @+p:Nat -> @+forward:Bool -> @+c:Nat -> Pair(NodeStore<K>, Nat)

template extreme_start source · line 1055 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @nodes:NodeStore<K> -> @+n:Nat -> @+id:Nat -> @+forward:Bool -> Pair(NodeStore<K>, Nat)

template ns_pop_n source · line 1062 · raw

@-K:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @used:Nat -> @tags:Array<Nat> -> @lefts:Array<Nat> -> @rights:Array<Nat> -> @parents:Array<Nat> -> @keys:Array<Maybe<&2, K>> -> Pair(NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Node<K>>)

template read source · line 1069 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id:Nat -> Pair(TreeMap<K, V, cmp>, Node<K>)

template get source · line 1076 · raw

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

template contains_key source · line 1079 · raw

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

template extreme source · line 1083 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id:Nat -> @+forward:Bool -> Pair(TreeMap<K, V, cmp>, Nat)

template neighbor_node source · line 1087 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+id:Nat -> @+forward:Bool -> @r:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, Nat)

template replace source · line 1091 · raw

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

template iter_child source · line 1094 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @payloads:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>> -> @+id:Nat -> @lower:Bound<K> -> @upper:Bound<K> -> @+forward:Bool -> @entry:Entry<K, V> -> @+p:Nat -> @r:Pair(NodeStore<K>, Nat) -> Pair(Cursor<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template iterator_reseek source · line 1098 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @k:Maybe<&2, K> -> @lower:Bound<K> -> @upper:Bound<K> -> @+forward:Bool -> @r:Pair(TreeMap<K, V, cmp>, Maybe<&2, V>) -> Pair(Cursor<K, V, cmp>, Maybe<&2, V>)

template replace_if_equal source · line 1105 · raw

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

template ns_pop source · line 1108 · raw

@-K:Data -> @s:NodeStore<K> -> Pair(NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Node<K>>)

template rotate_left_2 source · line 1112 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+x:Nat -> @+xn:Node<K> -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> TreeMap<K, V, cmp>

template rotate_right_2 source · line 1116 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+x:Nat -> @+xn:Node<K> -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> TreeMap<K, V, cmp>

template probe source · line 1120 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id:Nat -> @+k:K -> Pair(TreeMap<K, V, cmp>, Pair(Node<K>, Cmp))

template ascend_loop source · line 1123 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+fuel:Nat -> @+forward:Bool -> @st:Pair(TreeMap<K, V, cmp>, Ascend) -> Pair(TreeMap<K, V, cmp>, Nat)

template neighbor source · line 1132 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id:Nat -> @+forward:Bool -> Pair(TreeMap<K, V, cmp>, Nat)

template set_key source · line 1135 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id:Nat -> @+k:K -> TreeMap<K, V, cmp>

template refresh_ends_2 source · line 1138 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+r:Nat -> @pair_result:Pair(TreeMap<K, V, cmp>, Nat) -> TreeMap<K, V, cmp>

template key_id source · line 1142 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @r:Pair(TreeMap<K, V, cmp>, Nat) -> Pair(TreeMap<K, V, cmp>, Maybe<&2, K>)

template get_or_default source · line 1146 · raw

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

template view_get_checked source · line 1150 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+k:K -> @lower:Bound<K> -> @upper:Bound<K> -> @+descending:Bool -> @+valid:Bool -> Pair(View<K, V, cmp>, Maybe<&2, V>)

template iter_link source · line 1157 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @payloads:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>> -> @+i:Nat -> @lower:Bound<K> -> @upper:Bound<K> -> @+forward:Bool -> @entry:Entry<K, V> -> @r:Pair(NodeStore<K>, Nat) -> Pair(Cursor<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template iterator_has_next source · line 1161 · raw

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

template rotate_left_1 source · line 1165 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+x:Nat -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> TreeMap<K, V, cmp>

template rotate_right_1 source · line 1169 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+x:Nat -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> TreeMap<K, V, cmp>

template search_loop source · line 1173 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+fuel:Nat -> @+k:K -> @+id:Nat -> @+p:Nat -> @+on_left:Bool -> @st:Pair(TreeMap<K, V, cmp>, Pair(Node<K>, Cmp)) -> Pair(TreeMap<K, V, cmp>, Search)

template append_values source · line 1186 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @nodes:NodeStore<K> -> @+k:K -> @+v:V -> @+id:Nat -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>) -> Pair(TreeMap<K, V, cmp>, Result<&2, &2, Rejected<K, V>, Nat>)

template copy_key source · line 1193 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+target:Nat -> @+node:Node<K> -> TreeMap<K, V, cmp>

template refresh_ends_1 source · line 1200 · raw

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

template nav_equal source · line 1204 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id:Nat -> @+higher:Bool -> @+inclusive:Bool -> Pair(TreeMap<K, V, cmp>, Nat)

template first_key source · line 1212 · raw

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

template last_key source · line 1215 · raw

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

template view_get source · line 1218 · raw

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

template iter_valid source · line 1222 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @payloads:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>> -> @nodes:NodeStore<K> -> @+i:Nat -> @+current:Nat -> @lower:Bound<K> -> @upper:Bound<K> -> @+forward:Bool -> @entry:Entry<K, V> -> @+valid:Bool -> Pair(Cursor<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template rotate_left source · line 1229 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+x:Nat -> TreeMap<K, V, cmp>

template rotate_right source · line 1232 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+x:Nat -> TreeMap<K, V, cmp>

template append_nodes source · line 1235 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @payloads:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>> -> @+k:K -> @+v:V -> @+id:Nat -> @r:Pair(NodeStore<K>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>) -> Pair(TreeMap<K, V, cmp>, Result<&2, &2, Rejected<K, V>, Nat>)

template move_successor_2 source · line 1242 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+target:Nat -> @+source:Nat -> @+source_node:Node<K> -> @pair_result:Pair(TreeMap<K, V, cmp>, Maybe<&2, V>) -> Pair(TreeMap<K, V, cmp>, Nat)

template refresh_ends source · line 1246 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> TreeMap<K, V, cmp>

template nav_loop source · line 1249 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+fuel:Nat -> @+k:K -> @+higher:Bool -> @+inclusive:Bool -> @+id:Nat -> @+best:Nat -> @st:Pair(TreeMap<K, V, cmp>, Pair(Node<K>, Cmp)) -> Pair(TreeMap<K, V, cmp>, Nat)

template nav_end source · line 1262 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @payloads:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>> -> @+higher:Bool -> @+inclusive:Bool -> @r:Pair(NodeStore<K>, NavEnd) -> Pair(TreeMap<K, V, cmp>, Nat)

template iter_kv source · line 1269 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @payloads:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>> -> @nodes:NodeStore<K> -> @+i:Nat -> @+current:Nat -> @+lower:Bound<K> -> @+upper:Bound<K> -> @+forward:Bool -> @mk:Maybe<&2, K> -> @mv:Maybe<&2, V> -> Pair(Cursor<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template view_contains_key source · line 1276 · raw

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

template insert_black_left source · line 1279 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+z:Nat -> @+p:Nat -> @+g:Nat -> @+triangle:Bool -> Pair(TreeMap<K, V, cmp>, Fix)

template insert_black_right source · line 1286 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+z:Nat -> @+p:Nat -> @+g:Nat -> @+triangle:Bool -> Pair(TreeMap<K, V, cmp>, Fix)

template append_count source · line 1293 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @payloads:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>> -> @+k:K -> @+v:V -> @+p:Nat -> @r:Pair(NodeStore<K>, Nat) -> Pair(TreeMap<K, V, cmp>, Result<&2, &2, Rejected<K, V>, Nat>)

template move_successor_1 source · line 1297 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+target:Nat -> @+source:Nat -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, Nat)

template delete_borrow_left source · line 1301 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+p:Nat -> @+w:Nat -> @+pn:Node<K> -> @+wn:Node<K> -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template delete_borrow_right source · line 1304 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+p:Nat -> @+w:Nat -> @+pn:Node<K> -> @+wn:Node<K> -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template navigate source · line 1307 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+k:K -> @+higher:Bool -> @+inclusive:Bool -> Pair(TreeMap<K, V, cmp>, Nat)

template iter_key source · line 1311 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @payloads:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>> -> @+i:Nat -> @+current:Nat -> @lower:Bound<K> -> @upper:Bound<K> -> @+forward:Bool -> @mv:Maybe<&2, V> -> @r:Pair(NodeStore<K>, Maybe<&2, K>) -> Pair(Cursor<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template insert_uncle_left source · line 1315 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+z:Nat -> @+p:Nat -> @+g:Nat -> @+u:Nat -> @+triangle:Bool -> @+uncle:Node<K> -> Pair(TreeMap<K, V, cmp>, Fix)

template insert_uncle_right source · line 1322 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+z:Nat -> @+p:Nat -> @+g:Nat -> @+u:Nat -> @+triangle:Bool -> @+uncle:Node<K> -> Pair(TreeMap<K, V, cmp>, Fix)

template append source · line 1329 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+k:K -> @+v:V -> @+p:Nat -> Pair(TreeMap<K, V, cmp>, Result<&2, &2, Rejected<K, V>, Nat>)

template move_successor source · line 1333 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+target:Nat -> @+source:Nat -> Pair(TreeMap<K, V, cmp>, Nat)

template delete_borrow_read_left_2 source · line 1336 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+p:Nat -> @+pn:Node<K> -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template delete_borrow_read_right_2 source · line 1340 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+p:Nat -> @+pn:Node<K> -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template lower_key source · line 1344 · raw

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

template floor_key source · line 1347 · raw

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

template ceiling_key source · line 1350 · raw

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

template higher_key source · line 1353 · raw

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

template lower_entry source · line 1356 · raw

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

template floor_entry source · line 1359 · raw

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

template ceiling_entry source · line 1362 · raw

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

template higher_entry source · line 1365 · raw

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

template range_start source · line 1368 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @bound:Bound<K> -> @+forward:Bool -> Pair(TreeMap<K, V, cmp>, Nat)

template iter_value source · line 1377 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+i:Nat -> @+current:Nat -> @lower:Bound<K> -> @upper:Bound<K> -> @+forward:Bool -> @r:Pair(TreeMap<K, V, cmp>, Maybe<&2, V>) -> Pair(Cursor<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template insert_side_left_1 source · line 1381 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+z:Nat -> @+p:Nat -> @+g:Nat -> @+pn:Node<K> -> @+gn:Node<K> -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, Fix)

template insert_side_right_1 source · line 1385 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+z:Nat -> @+p:Nat -> @+g:Nat -> @+pn:Node<K> -> @+gn:Node<K> -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, Fix)

template allocate source · line 1389 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+p:Nat -> @+k:K -> @+v:V -> Pair(TreeMap<K, V, cmp>, Result<&2, &2, Rejected<K, V>, Nat>)

template successor_ready source · line 1397 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+target:Nat -> @r:Pair(TreeMap<K, V, cmp>, Nat) -> Pair(TreeMap<K, V, cmp>, Nat)

template delete_borrow_read_left_1 source · line 1401 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+p:Nat -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template delete_borrow_read_right_1 source · line 1405 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+p:Nat -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template view_iterator source · line 1409 · raw

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

template iter_at source · line 1413 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+next:Nat -> @+current:Nat -> @lower:Bound<K> -> @upper:Bound<K> -> @+forward:Bool -> @m:TreeMap<K, V, cmp> -> Pair(Cursor<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template view_nav_start source · line 1420 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+k:K -> @lower:Bound<K> -> @upper:Bound<K> -> @+higher:Bool -> @+inclusive:Bool -> @+within:Bool -> Pair(TreeMap<K, V, cmp>, Nat)

template view_extreme source · line 1427 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @view:View<K, V, cmp> -> @+first:Bool -> Pair(View<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template insert_side_left source · line 1432 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+z:Nat -> @+p:Nat -> @+g:Nat -> @+pn:Node<K> -> @+gn:Node<K> -> Pair(TreeMap<K, V, cmp>, Fix)

template insert_side_right source · line 1435 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+z:Nat -> @+p:Nat -> @+g:Nat -> @+pn:Node<K> -> @+gn:Node<K> -> Pair(TreeMap<K, V, cmp>, Fix)

template delete_target source · line 1438 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+id:Nat -> @r:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, Nat)

template delete_borrow_read_left source · line 1446 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+p:Nat -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template delete_borrow_read_right source · line 1449 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+p:Nat -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template iterator_next source · line 1452 · raw

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

template view_nav source · line 1456 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @view:View<K, V, cmp> -> @+k:K -> @+higher:Bool -> @+inclusive:Bool -> Pair(View<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template view_first_entry source · line 1461 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @view:View<K, V, cmp> -> Pair(View<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template view_last_entry source · line 1464 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @view:View<K, V, cmp> -> Pair(View<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template insert_side source · line 1467 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+z:Nat -> @+p:Nat -> @+g:Nat -> @+pn:Node<K> -> @+gn:Node<K> -> @+on_left:Bool -> Pair(TreeMap<K, V, cmp>, Fix)

template delete_far_left source · line 1474 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+p:Nat -> @+w:Nat -> @+pn:Node<K> -> @+wn:Node<K> -> @+far_red:Bool -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template delete_far_right source · line 1481 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+p:Nat -> @+w:Nat -> @+pn:Node<K> -> @+wn:Node<K> -> @+far_red:Bool -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template iterator_next_key source · line 1488 · raw

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

template iterator_next_value source · line 1491 · raw

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

template contains_value_loop source · line 1494 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-eq:(@_:V -> @_:V -> Bool) -> @+fuel:Nat -> @+wanted:V -> @+found:Bool -> @st:Pair(Cursor<K, V, cmp>, Maybe<&2, Entry<K, V>>) -> Pair(TreeMap<K, V, cmp>, Bool)

template view_lower_entry source · line 1505 · raw

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

template view_floor_entry source · line 1508 · raw

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

template view_ceiling_entry source · line 1511 · raw

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

template view_higher_entry source · line 1514 · raw

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

template view_count_loop source · line 1517 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+fuel:Nat -> @+count:Nat -> @st:Pair(Cursor<K, V, cmp>, Maybe<&2, Entry<K, V>>) -> Pair(View<K, V, cmp>, Nat)

template view_clear_next source · line 1526 · raw

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

template insert_grand_1 source · line 1530 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+z:Nat -> @+p:Nat -> @+pn:Node<K> -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, Fix)

template delete_children_left source · line 1534 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+p:Nat -> @+w:Nat -> @+pn:Node<K> -> @+wn:Node<K> -> @+near_red:Bool -> @+far_red:Bool -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template delete_children_right source · line 1541 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+p:Nat -> @+w:Nat -> @+pn:Node<K> -> @+wn:Node<K> -> @+near_red:Bool -> @+far_red:Bool -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template contains_value_start source · line 1548 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-eq:(@_:V -> @_:V -> Bool) -> @+wanted:V -> @r:Pair(TreeMap<K, V, cmp>, Nat) -> Pair(TreeMap<K, V, cmp>, Bool)

template view_size source · line 1552 · raw

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

template insert_grand source · line 1556 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+z:Nat -> @+p:Nat -> @+pn:Node<K> -> Pair(TreeMap<K, V, cmp>, Fix)

template delete_sibling_left_4 source · line 1559 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+p:Nat -> @+pn:Node<K> -> @+wn:Node<K> -> @+near_node:Node<K> -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template delete_sibling_right_4 source · line 1563 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+p:Nat -> @+pn:Node<K> -> @+wn:Node<K> -> @+near_node:Node<K> -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template contains_value source · line 1567 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-eq:(@_:V -> @_:V -> Bool) -> @m:TreeMap<K, V, cmp> -> @+wanted:V -> Pair(TreeMap<K, V, cmp>, Bool)

template insert_parent source · line 1570 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+z:Nat -> @+p:Nat -> @+pn:Node<K> -> @+is_red:Bool -> Pair(TreeMap<K, V, cmp>, Fix)

template delete_sibling_left_3 source · line 1577 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+p:Nat -> @+pn:Node<K> -> @+wn:Node<K> -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template delete_sibling_right_3 source · line 1581 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+p:Nat -> @+pn:Node<K> -> @+wn:Node<K> -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template insert_fix_step_2 source · line 1585 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+z:Nat -> @+zn:Node<K> -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, Fix)

template delete_sibling_left_2 source · line 1589 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+p:Nat -> @+pn:Node<K> -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template delete_sibling_right_2 source · line 1593 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+p:Nat -> @+pn:Node<K> -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template insert_fix_step_1 source · line 1597 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+z:Nat -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, Fix)

template delete_sibling_left_1 source · line 1601 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+p:Nat -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template delete_sibling_right_1 source · line 1605 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+p:Nat -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template insert_fix_step source · line 1609 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+z:Nat -> Pair(TreeMap<K, V, cmp>, Fix)

template delete_sibling_left source · line 1612 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+p:Nat -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template delete_sibling_right source · line 1615 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+p:Nat -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template insert_fix_loop source · line 1618 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+fuel:Nat -> @st:Pair(TreeMap<K, V, cmp>, Fix) -> TreeMap<K, V, cmp>

template delete_red_sibling_left source · line 1627 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+p:Nat -> @+w:Nat -> @+red_sibling:Bool -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template delete_red_sibling_right source · line 1634 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+p:Nat -> @+w:Nat -> @+red_sibling:Bool -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template insert_fixed source · line 1641 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+id:Nat -> @r:Pair(TreeMap<K, V, cmp>, Nat) -> TreeMap<K, V, cmp>

template delete_side_left_1 source · line 1645 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+p:Nat -> @+pn:Node<K> -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template delete_side_right_1 source · line 1649 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+p:Nat -> @+pn:Node<K> -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template put_allocated source · line 1653 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+p:Nat -> @+on_left:Bool -> @r:Pair(TreeMap<K, V, cmp>, Result<&2, &2, Rejected<K, V>, Nat>) -> Pair(TreeMap<K, V, cmp>, Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>)

template delete_side_left source · line 1660 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+p:Nat -> @+pn:Node<K> -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template delete_side_right source · line 1663 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+p:Nat -> @+pn:Node<K> -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template put_found source · line 1666 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+v:V -> @r:Pair(TreeMap<K, V, cmp>, Search) -> Pair(TreeMap<K, V, cmp>, Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>)

template delete_side source · line 1673 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+x:Nat -> @+p:Nat -> @+pn:Node<K> -> @+on_left:Bool -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template put_absent_found source · line 1680 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+k:K -> @+v:V -> @r:Pair(TreeMap<K, V, cmp>, Search) -> Pair(TreeMap<K, V, cmp>, Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>)

template put source · line 1687 · raw

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

template delete_stop source · line 1690 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+x:Nat -> @+p:Nat -> @+pn:Node<K> -> @+stop:Bool -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template put_if_absent source · line 1697 · raw

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

template delete_fix_step_3 source · line 1700 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+x:Nat -> @+p:Nat -> @+root_node:Nat -> @+xn:Node<K> -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template view_put_checked source · line 1704 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+k:K -> @+v:V -> @lower:Bound<K> -> @upper:Bound<K> -> @+descending:Bool -> @+valid:Bool -> Pair(View<K, V, cmp>, Result<&2, &2, Rejected<K, V>, Maybe<&2, V>>)

template delete_fix_step_2 source · line 1711 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+x:Nat -> @+p:Nat -> @+root_node:Nat -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template view_put source · line 1715 · raw

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

template delete_fix_step_1 source · line 1719 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+x:Nat -> @+p:Nat -> @pair_result:Pair(TreeMap<K, V, cmp>, Nat) -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template delete_fix_step source · line 1723 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+x:Nat -> @+p:Nat -> Pair(TreeMap<K, V, cmp>, DeleteFix)

template delete_fix_loop source · line 1726 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+fuel:Nat -> @st:Pair(TreeMap<K, V, cmp>, DeleteFix) -> TreeMap<K, V, cmp>

template delete_repair source · line 1735 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+x:Nat -> @+p:Nat -> @+was_red:Bool -> TreeMap<K, V, cmp>

template unlink_2 source · line 1739 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+id:Nat -> @+node:Node<K> -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> TreeMap<K, V, cmp>

template unlink_1 source · line 1743 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+id:Nat -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> TreeMap<K, V, cmp>

template unlink source · line 1747 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id:Nat -> TreeMap<K, V, cmp>

template unlink_target source · line 1750 · raw

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

template remove_present_1 source · line 1754 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+id:Nat -> @pair_result:Pair(TreeMap<K, V, cmp>, Maybe<&2, V>) -> Pair(TreeMap<K, V, cmp>, Maybe<&2, V>)

template remove_present source · line 1758 · raw

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

template remove_id source · line 1761 · raw

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

template remove_found source · line 1768 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @r:Pair(TreeMap<K, V, cmp>, Search) -> Pair(TreeMap<K, V, cmp>, Maybe<&2, V>)

template remove_entry_id_1 source · line 1772 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+id:Nat -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(TreeMap<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template iterator_delete_1 source · line 1776 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+current:Nat -> @lower:Bound<K> -> @upper:Bound<K> -> @+forward:Bool -> @pair_result:Pair(TreeMap<K, V, cmp>, Node<K>) -> Pair(Cursor<K, V, cmp>, Maybe<&2, V>)

template remove_if_apply source · line 1780 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id:Nat -> @+replacement:V -> @+equal:Bool -> Pair(TreeMap<K, V, cmp>, Bool)

template remove source · line 1787 · raw

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

template remove_entry_id source · line 1790 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id:Nat -> Pair(TreeMap<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template iterator_delete source · line 1793 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+next:Nat -> @+current:Nat -> @lower:Bound<K> -> @upper:Bound<K> -> @+forward:Bool -> Pair(Cursor<K, V, cmp>, Maybe<&2, V>)

template remove_if_value source · line 1796 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-eq:(@_:V -> @_:V -> Bool) -> @+id:Nat -> @+expected:V -> @+replacement:V -> @r:Pair(TreeMap<K, V, cmp>, Maybe<&2, V>) -> Pair(TreeMap<K, V, cmp>, Bool)

template poll_ready source · line 1803 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @r:Pair(TreeMap<K, V, cmp>, Nat) -> Pair(TreeMap<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template view_remove_checked source · line 1807 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+k:K -> @lower:Bound<K> -> @upper:Bound<K> -> @+descending:Bool -> @+valid:Bool -> Pair(View<K, V, cmp>, Maybe<&2, V>)

template iterator_remove source · line 1814 · raw

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

template remove_if_found source · line 1818 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @-eq:(@_:V -> @_:V -> Bool) -> @+expected:V -> @+replacement:V -> @r:Pair(TreeMap<K, V, cmp>, Search) -> Pair(TreeMap<K, V, cmp>, Bool)

template poll_first_entry source · line 1822 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> Pair(TreeMap<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template poll_last_entry source · line 1825 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> Pair(TreeMap<K, V, cmp>, Maybe<&2, Entry<K, V>>)

template view_remove source · line 1828 · raw

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

template remove_if_equal source · line 1832 · raw

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

template view_clear_loop source · line 1835 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+fuel:Nat -> @st:Pair(Cursor<K, V, cmp>, Maybe<&2, Entry<K, V>>) -> View<K, V, cmp>

template view_clear source · line 1844 · raw

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