src/containers/balanced_search_tree.bend checks

raw source on the hub · import 0x9ee2e9a299991dcc089fe22c7f3ceb5f/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 TreeMap source · line 13 · 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:0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/dynamic_array.DynArray<&2, Node<K>> -> @payloads:0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>> -> TreeMap<K, V, cmp>

type Entry source · line 17 · raw

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

Entry

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

type Error source · line 20 · raw

Data

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

type Rejected source · line 26 · raw

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

Rejected

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

type Search source · line 29 · raw

Data

Search

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

type Fix source · line 32 · raw

Data

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

type Ascend source · line 35 · raw

Data

Ascend

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

type DeleteFix source · line 40 · 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 Bound source · line 43 · 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 48 · 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 51 · 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 54 · 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 pick source · line 58 · raw

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

def ascend_choice source · line 175 · raw

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

def ordering_ok source · line 230 · raw

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

Templates

template node_red source · line 65 · raw

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

template node_left source · line 72 · raw

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

template node_right source · line 79 · raw

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

template node_parent source · line 86 · raw

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

template node_key source · line 93 · raw

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

template new source · line 100 · raw

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

template size source · line 103 · 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 107 · 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 111 · 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 115 · 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 119 · raw

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

template write_finish source · line 126 · raw

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

template set_root source · line 130 · 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 134 · 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 exchange_finish source · line 141 · raw

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

template append_rollback source · line 148 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @payloads:0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>> -> @+k:K -> @+v:V -> @r:Pair(0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/dynamic_array.DynArray<&2, Node<K>>, Result<&2, &2, 0x9ee2e9a299991dcc089fe22c7f3ceb5f/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 152 · 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 156 · 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 160 · 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 164 · raw

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

template contains_found source · line 171 · raw

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

template node_slot_done source · line 182 · raw

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

template neighbor_slots_finish source · line 189 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+n:Nat -> @+root:Nat -> @+lo:Nat -> @+hi:Nat -> @+free:Nat -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+used:Nat -> @payloads:0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/dynamic_array.DynArray<&2, Maybe<&2, V>> -> @r:Pair(Array<Maybe<&2, Node<K>>>, Nat) -> Pair(TreeMap<K, V, cmp>, Nat)

template move_successor_3 source · line 193 · 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 197 · 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 201 · raw

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

template clear source · line 205 · raw

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

template is_empty_1 source · line 209 · 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 213 · 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 with_limit source · line 220 · raw

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

template default_value source · line 223 · 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 239 · 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 246 · 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 249 · 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 252 · raw

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

template view_reverse source · line 255 · raw

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

template view_finish source · line 259 · raw

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

template view_value source · line 263 · 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 267 · 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 271 · 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 275 · raw

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

template iterator_view source · line 279 · raw

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

template iterator_yield source · line 283 · 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 287 · 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 294 · 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 298 · 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 305 · 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 312 · 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 319 · 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 326 · 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 child source · line 333 · raw

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

template read source · line 338 · raw

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

template write source · line 345 · raw

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

template exchange source · line 352 · 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 append_values source · line 359 · raw

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

template insert_header source · line 366 · 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 370 · 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 377 · 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 node_slot_checked source · line 384 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @nodes:Array<Maybe<&2, Node<K>>> -> @+i:Nat -> @+valid:Bool -> Pair(Array<Maybe<&2, Node<K>>>, Node<K>)

template ascend_slots_step source · line 391 · raw

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

template refresh_ends_3 source · line 398 · 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 402 · 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 405 · 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 above_lower source · line 409 · raw

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

template below_upper source · line 418 · raw

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

template bounds_valid source · line 427 · raw

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

template range_unbounded source · line 442 · 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 449 · raw

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

template descending_iterator source · line 452 · raw

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

template set_left_node source · line 455 · raw

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

template set_right_node source · line 462 · raw

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

template set_parent_node source · line 469 · raw

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

template set_red_node source · line 476 · raw

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

template probe source · line 483 · 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 append_nodes source · line 486 · raw

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

template reuse_slot source · line 493 · 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 get_found source · line 496 · 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 extreme_probe source · line 500 · raw

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

template ascend_loop source · line 504 · 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 node_slot source · line 513 · raw

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

template extreme_slots_probe source · line 520 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+forward:Bool -> @r:Pair(Array<Maybe<&2, Node<K>>>, Node<K>) -> Pair(Array<Maybe<&2, Node<K>>>, Nat)

template set_key_node source · line 524 · 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 531 · raw

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

template key_id source · line 535 · 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 entry_snapshot_value source · line 539 · raw

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

template replace_found source · line 543 · 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 550 · raw

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

template sub_map source · line 553 · 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 556 · 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 563 · raw

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

template key_set source · line 566 · raw

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

template values source · line 569 · raw

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

template replace_if_apply source · line 572 · 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 set_left_1 source · line 579 · raw

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

template set_right_1 source · line 583 · raw

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

template set_parent_1 source · line 587 · raw

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

template set_red_1 source · line 591 · raw

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

template search_loop source · line 595 · 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_count source · line 608 · raw

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

template alloc_read source · line 612 · 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 extreme_loop source · line 619 · raw

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

template ascend_slots_loop source · line 628 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+fuel:Nat -> @+used:Nat -> @+forward:Bool -> @st:Pair(Array<Maybe<&2, Node<K>>>, Ascend) -> Pair(Array<Maybe<&2, Node<K>>>, Nat)

template extreme_slots_loop source · line 637 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @+fuel:Nat -> @+used:Nat -> @+forward:Bool -> @+id:Nat -> @st:Pair(Array<Maybe<&2, Node<K>>>, Nat) -> Pair(Array<Maybe<&2, Node<K>>>, Nat)

template set_key_1 source · line 646 · 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 first_key source · line 650 · 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 653 · raw

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

template entry_snapshot source · line 656 · 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 replace_if_value source · line 660 · 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 667 · 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 674 · 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 set_left source · line 681 · 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 684 · 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 687 · raw

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

template set_red source · line 690 · raw

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

template search source · line 693 · raw

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

template append source · line 697 · 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 extreme source · line 701 · 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_slots source · line 706 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @nodes:Array<Maybe<&2, Node<K>>> -> @+n:Nat -> @+used:Nat -> @+id:Nat -> @+p:Nat -> @+forward:Bool -> @+c:Nat -> Pair(Array<Maybe<&2, Node<K>>>, Nat)

template set_key source · line 713 · raw

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

template first_entry source · line 716 · 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 719 · 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 replace_if_found source · line 722 · 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 iterator_has_next source · line 726 · raw

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

template attach_side source · line 730 · 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 black_root_1 source · line 739 · raw

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

template allocate source · line 743 · 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 get source · line 751 · 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 754 · raw

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

template neighbor_node source · line 757 · 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 copy_key source · line 761 · 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_2 source · line 768 · raw

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

template replace source · line 772 · 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 iterator_reseek source · line 775 · 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 782 · 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 attach source · line 785 · 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 black_root source · line 788 · raw

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

template neighbor source · line 792 · 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 move_successor_2 source · line 795 · 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_1 source · line 799 · raw

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

template get_or_default source · line 803 · 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 807 · 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 rotate_left_3 source · line 814 · 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 818 · 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 move_successor_1 source · line 822 · 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 refresh_ends source · line 826 · raw

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

template nav_equal source · line 829 · 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 view_get source · line 836 · 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 iterator_checked source · line 840 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:TreeMap<K, V, cmp> -> @+id: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_2 source · line 847 · 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 851 · 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 move_successor source · line 855 · 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 nav_loop source · line 858 · 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 iterator_read source · line 871 · raw

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

template view_contains_key source · line 878 · raw

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

template rotate_left_1 source · line 881 · 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 885 · 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 successor_ready source · line 889 · 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 navigate source · line 893 · 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 iterator_next source · line 897 · 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 rotate_left source · line 901 · 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 904 · raw

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

template delete_target source · line 907 · 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 lower_key source · line 915 · 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 918 · 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 921 · 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 924 · 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 927 · 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 930 · 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 933 · 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 936 · 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 939 · 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 iterator_next_key source · line 948 · 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 951 · 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 954 · 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_count_loop source · line 965 · 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 974 · 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_black_left source · line 978 · 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 985 · 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 delete_borrow_left source · line 992 · 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 995 · 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 view_iterator source · line 998 · raw

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

template contains_value_start source · line 1002 · 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_nav_start source · line 1006 · 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 1013 · 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_uncle_left source · line 1018 · 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 1025 · 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 delete_borrow_read_left_2 source · line 1032 · 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 1036 · 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 contains_value source · line 1040 · 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 view_nav source · line 1043 · 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 1048 · 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 1051 · 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_size source · line 1054 · raw

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

template insert_side_left_1 source · line 1058 · 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 1062 · 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 delete_borrow_read_left_1 source · line 1066 · 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 1070 · 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_lower_entry source · line 1074 · 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 1077 · 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 1080 · 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 1083 · 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 insert_side_left source · line 1086 · 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 1089 · 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_borrow_read_left source · line 1092 · 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 1095 · raw

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

template insert_side source · line 1098 · 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 1105 · 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 1112 · 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 insert_grand_1 source · line 1119 · 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 1123 · 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 1130 · 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 insert_grand source · line 1137 · 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 1140 · 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 1144 · 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 insert_parent source · line 1148 · 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 1155 · 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 1159 · 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 1163 · 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 1167 · 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 1171 · 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 1175 · 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 1179 · 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 1183 · 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 1187 · 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 1190 · 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 1193 · 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 1196 · 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 1205 · 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 1212 · 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 1219 · 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 1223 · 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 1227 · 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 1231 · 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 1238 · 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 1241 · 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 1244 · 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 1251 · 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 1258 · 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 1265 · 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 1268 · 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 1275 · 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 1278 · 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 1282 · 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 1289 · 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 1293 · 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 1297 · 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 1301 · 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 1304 · 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 1313 · 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 1317 · 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 1321 · 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 1325 · 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 1328 · 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 1332 · 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 1336 · 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 1339 · 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 1346 · 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 1350 · 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 1354 · 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 1358 · 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 1365 · 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 1368 · 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 1371 · 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 1374 · 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 1381 · 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 1385 · 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 1392 · 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 1396 · 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 1400 · 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 1403 · 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 1406 · 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 1410 · 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 1413 · 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 1422 · raw

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