spec/containers/doubly_linked_list.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/spec/containers/doubly_linked_list.bend as Doubly_linked_list

4 imports

import Base
import ../lib/common.bend as C
import ../../src/containers/types/doubly_linked_list.bend as E
import ../lib/sequence.bend as V

Types

type DS source · line 19 · raw

@-T:Data -> Data

DS

@-T:Data -> @tag:U32 -> @order:List<&2, Nat> -> @vals:List<&2, Maybe<&2, T>> -> @gens:List<&2, U32> -> @free:List<&2, Nat> -> DS<T>

type Pos source · line 161 · raw

Data

where a new element goes

PFront
```
Pos
```
PBack
```
Pos
```
PBefore
```
@i:Nat -> Pos
```
PAfter
```
@i:Nat -> Pos
```

Definitions

def pick_list source · line 22 · raw

@+b:Bool -> @xs:List<&2, Nat> -> @ys:List<&2, Nat> -> List<&2, Nat>

def pick_maybe source · line 29 · raw

@+b:Bool -> @x:Maybe<&2, Nat> -> @y:Maybe<&2, Nat> -> Maybe<&2, Nat>

def cons_some source · line 36 · raw

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

def maybe_done source · line 43 · raw

@-T:Data -> @e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error -> @m:Maybe<&2, T> -> Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, T>

def gen_of source · line 50 · raw

@+gens:List<&2, U32> -> @+i:Nat -> U32

def val_of source · line 59 · raw

@-T:Data -> @+vals:List<&2, Maybe<&2, T>> -> @+i:Nat -> Maybe<&2, T>

def handle source · line 68 · raw

@+tag:U32 -> @+gens:List<&2, U32> -> @+i:Nat -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle

def live_gen source · line 73 · raw

@-T:Data -> @m:Maybe<&2, T> -> @+same:Bool -> Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>

def valid_own source · line 82 · raw

@-T:Data -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+i:Nat -> @+g:U32 -> @mine:Bool -> Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>

def validate source · line 90 · raw

@-T:Data -> @+s:DS<T> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>

None when h names a live element of the list at its current generation

def ins_before source · line 97 · raw

@xs:List<&2, Nat> -> @+i:Nat -> @+n:Nat -> List<&2, Nat>

def ins_after source · line 104 · raw

@xs:List<&2, Nat> -> @+i:Nat -> @+n:Nat -> List<&2, Nat>

def delete source · line 111 · raw

@xs:List<&2, Nat> -> @+i:Nat -> List<&2, Nat>

def first source · line 118 · raw

@xs:List<&2, Nat> -> Maybe<&2, Nat>

def after source · line 126 · raw

@xs:List<&2, Nat> -> @+i:Nat -> Maybe<&2, Nat>

the element after i

def before source · line 134 · raw

@xs:List<&2, Nat> -> @+i:Nat -> @p:Maybe<&2, Nat> -> Maybe<&2, Nat>

the element before i (p: the element before the list)

def values source · line 141 · raw

@-T:Data -> @+vals:List<&2, Maybe<&2, T>> -> @xs:List<&2, Nat> -> List<&2, T>

def alloc source · line 151 · raw

@-T:Data -> @s:DS<T> -> Pair(DS<T>, Nat)

the id a new element takes, the list with the id reserved

def place_order source · line 167 · raw

@pos:Pos -> @xs:List<&2, Nat> -> @+n:Nat -> List<&2, Nat>

def place source · line 179 · raw

@-T:Data -> @s:DS<T> -> @+n:Nat -> @x:T -> @pos:Pos -> Pair(DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle)

store x at the reserved id n and place n in the order

def inserted source · line 184 · raw

@-T:Data -> @r:Pair(DS<T>, Nat) -> @x:T -> @pos:Pos -> Pair(DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle)

def push_front source · line 189 · raw

@-T:Data -> @s:DS<T> -> @x:T -> Pair(DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle)

def push_back source · line 192 · raw

@-T:Data -> @s:DS<T> -> @x:T -> Pair(DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle)

def retire source · line 197 · raw

@+gens:List<&2, U32> -> @+i:Nat -> @+free:List<&2, Nat> -> @+g:U32 -> @exhausted:Bool -> Pair(List<&2, U32>, List<&2, Nat>)

def removed source · line 204 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+i:Nat -> @+v:T -> @r:Pair(List<&2, U32>, List<&2, Nat>) -> Pair(DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)

def remove_m source · line 209 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+i:Nat -> @m:Maybe<&2, T> -> Pair(DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)

def remove_live source · line 216 · raw

@-T:Data -> @s:DS<T> -> @+i:Nat -> Pair(DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)

def get_live source · line 223 · raw

@-T:Data -> @s:DS<T> -> @+i:Nat -> Pair(DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)

def set_live source · line 228 · raw

@-T:Data -> @s:DS<T> -> @+i:Nat -> @x:T -> Pair(DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)

def nbr source · line 233 · raw

@+tag:U32 -> @+gens:List<&2, U32> -> @m:Maybe<&2, Nat> -> Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>

def next_live source · line 240 · raw

@-T:Data -> @s:DS<T> -> @+i:Nat -> Pair(DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)

def prev_live source · line 245 · raw

@-T:Data -> @s:DS<T> -> @+i:Nat -> Pair(DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)

def ins_obs source · line 250 · raw

@-T:Data -> @r:Pair(DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle) -> Pair(DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)

def live_op source · line 255 · raw

@-T:Data -> @s:DS<T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> @+i:Nat -> Pair(DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)

def failed source · line 281 · raw

@-T:Data -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> @e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>

the observation of op failing with e (the list is unchanged)

def handle_id source · line 306 · raw

@+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> Nat

def checked source · line 311 · raw

@-T:Data -> @+s:DS<T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error> -> Pair(DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)

def with_handle source · line 318 · raw

@-T:Data -> @+s:DS<T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> Pair(DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)

def len_of source · line 321 · raw

@-T:Data -> @s:DS<T> -> Nat

def list_of source · line 326 · raw

@-T:Data -> @s:DS<T> -> List<&2, T>

def pushed source · line 331 · raw

@-T:Data -> @r:Pair(DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle) -> Pair(DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)

def step source · line 336 · raw

@-T:Data -> @+s:DS<T> -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> Pair(DS<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>)

def empty source · line 361 · raw

@-T:Data -> @+tag:U32 -> DS<T>

def cons_obs source · line 364 · raw

@-T:Data -> @o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T> -> @r:Pair(DS<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>>) -> Pair(DS<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>>)

def run source · line 369 · raw

@-T:Data -> @ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T>> -> @+s:DS<T> -> Pair(DS<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>>)

def nx source · line 421 · raw

@-T:Data -> @+s:DS<T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> DS<T>

def ob source · line 424 · raw

@-T:Data -> @+s:DS<T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Op<T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Obs<T>

def ord source · line 427 · raw

@-T:Data -> @s:DS<T> -> List<&2, Nat>

def vls source · line 432 · raw

@-T:Data -> @s:DS<T> -> List<&2, Maybe<&2, T>>

def gns source · line 437 · raw

@-T:Data -> @s:DS<T> -> List<&2, U32>

def has_of source · line 443 · raw

@m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error> -> Bool

Has_Element (Container, Position)

def has_element source · line 450 · raw

@-T:Data -> @+s:DS<T> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> Bool

def lastm source · line 454 · raw

@xs:List<&2, Nat> -> @p:Maybe<&2, Nat> -> Maybe<&2, Nat>

Previous: the last element of a, or p when a is empty

def FSplit source · line 462 · raw

@+i:Nat -> @+xs:List<&2, Nat> -> Type

---- the order split at a live id ----

def Next.next_position source · line 466 · raw

@+a:List<&2, Nat> -> @+i:Nat -> @+b:List<&2, Nat> -> Type

Next (1614)

def Previous.prev_position source · line 470 · raw

@+t:List<&2, Nat> -> @+x:Nat -> @+i:Nat -> @+b:List<&2, Nat> -> @+p:Maybe<&2, Nat> -> Type

Previous (1652)

def Has_Element.valid_live source · line 474 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{validate(T, DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> Type

Has_Element (1814)

def Length.length_result source · line 478 · raw

@-T:Data -> @+s:DS<T> -> Type

Length (78)

def Length.length_frame source · line 482 · raw

@-T:Data -> @+s:DS<T> -> Type

Length (78)

def Iteration.to_list_model source · line 486 · raw

@-T:Data -> @+s:DS<T> -> Type

iteration (Iter_Model)

def Iteration.to_list_frame source · line 490 · raw

@-T:Data -> @+s:DS<T> -> Type

iteration (Iter_Model)

def Empty_List.new_empty source · line 494 · raw

@-T:Data -> @+tag:U32 -> Type

Empty_List (71)

def Element.get_frame source · line 498 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{validate(T, DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> Type

Element (419)

def Element.get_element source · line 502 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{validate(T, DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+v:T -> @+hval:{val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>} -> Type

Element (419)

def Replace_Element.set_positions source · line 506 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{validate(T, DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> Type

Replace_Element (430)

def Replace_Element.set_gens source · line 510 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{validate(T, DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> Type

Replace_Element (430)

def Replace_Element.set_element source · line 514 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{validate(T, DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+v:T -> @+hval:{val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>} -> Type

Replace_Element (430)

def Replace_Element.set_others source · line 518 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{validate(T, DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+j:Nat -> @+ne:{Nat.is_eq(handle_id(h), j) == False{} : Bool} -> Type

Replace_Element (430)

def Prepend.push_front_positions source · line 522 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+x:T -> Type

Prepend (836)

def Prepend.push_front_first source · line 526 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+x:T -> Type

Prepend (836)

def Prepend.push_front_length source · line 530 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+x:T -> Type

Prepend (836)

def Append.push_back_positions source · line 534 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+x:T -> Type

Append (905)

def Append.push_back_last source · line 538 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+x:T -> Type

Append (905)

def Append.push_back_length source · line 542 · raw

@-T:Data -> @+tag:U32 -> @+order:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+x:T -> Type

Append (905)

def Insert.insert_before_equal source · line 546 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{validate(T, DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(handle_id(h), a) == False{} : Bool} -> Type

Insert Before (523)

def Insert.insert_before_at source · line 550 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{validate(T, DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(handle_id(h), a) == False{} : Bool} -> Type

Insert Before (523)

def Insert.insert_before_shifted source · line 554 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{validate(T, DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(handle_id(h), a) == False{} : Bool} -> Type

Insert Before (523)

def Insert.insert_before_length source · line 558 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{validate(T, DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(handle_id(h), a) == False{} : Bool} -> Type

Insert Before (523)

def Insert.insert_after_equal source · line 562 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{validate(T, DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(handle_id(h), a) == False{} : Bool} -> Type

Insert after (Next (Before))

def Insert.insert_after_at source · line 566 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{validate(T, DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(handle_id(h), a) == False{} : Bool} -> Type

Insert after (Next (Before))

def Insert.insert_after_shifted source · line 570 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{validate(T, DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(handle_id(h), a) == False{} : Bool} -> Type

Insert after (Next (Before))

def Insert.insert_after_length source · line 574 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+hv:{validate(T, DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(handle_id(h), a) == False{} : Bool} -> Type

Insert after (Next (Before))

def Delete.remove_result source · line 578 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{validate(T, DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+v:T -> @+hval:{val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>} -> Type

Delete (978)

def Delete.remove_equal source · line 582 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{validate(T, DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(handle_id(h), a) == False{} : Bool} -> @+v:T -> @+hval:{val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>} -> Type

Delete (978)

def Delete.remove_shifted source · line 586 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{validate(T, DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(handle_id(h), a) == False{} : Bool} -> @+v:T -> @+hval:{val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>} -> Type

Delete (978)

def Delete.remove_length source · line 590 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{validate(T, DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(handle_id(h), a) == False{} : Bool} -> @+v:T -> @+hval:{val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>} -> Type

Delete (978)

def Delete.remove_stale source · line 594 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{validate(T, DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+v:T -> @+hval:{val_of(T, vals, handle_id(h)) == Some{v} : Maybe<&2, T>} -> Type

Delete (978)

def Next.next_result source · line 598 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{validate(T, DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(handle_id(h), a) == False{} : Bool} -> Type

Next (1614)

def Next.next_frame source · line 602 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{validate(T, DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> Type

Next (1614)

def Previous.prev_result source · line 606 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{validate(T, DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> @+hn:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.memn(handle_id(h), a) == False{} : Bool} -> Type

Previous (1652)

def Previous.prev_first source · line 610 · raw

@-T:Data -> @+tag:U32 -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{validate(T, DS{tag, handle_id(h) <> b, vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> Type

Previous (1652)

def Previous.prev_frame source · line 614 · raw

@-T:Data -> @+tag:U32 -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+vals:List<&2, Maybe<&2, T>> -> @+gens:List<&2, U32> -> @+free:List<&2, Nat> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+hv:{validate(T, DS{tag, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, handle_id(h) <> b), vals, gens, free}, h) == None{} : Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>} -> Type

Previous (1652)