~/bend-docscommunity

proofs/containers/doubly_linked_list/direct.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/direct.bend as Direct

5 imports
import Base
import ../../../src/containers/doubly_linked_list.bend as D
import ../../../src/containers/internal/dlist_storage.bend as R
import ../../../src/containers/types/internal_dlist.bend as I
import ../../../src/containers/types/doubly_linked_list.bend as E

Templates

template gv source · line 13 · raw

@-T:Data -> @+tag:U32 -> @+depth:Nat -> @+cap:U32 -> @-gens:Array<U32> -> @p:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, T>) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.get_result(T, tag, depth, cap, gens, p) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_value(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.value_result(T, tag, depth, cap, gens, p)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, T>)}

template sv source · line 18 · raw

@-T:Data -> @+tag:U32 -> @+depth:Nat -> @+cap:U32 -> @-gens:Array<U32> -> @p:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/internal_dlist.Error, Unit>) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.set_result(T, tag, depth, cap, gens, p) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_unit(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.unit_result(T, tag, depth, cap, gens, p)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, Unit>)}

template get_m source · line 23 · raw

@-T:Data -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+tag:U32 -> @+depth:Nat -> @+cap:U32 -> @raw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DList<T> -> @gens:Array<U32> -> @m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.get_ready(T, h, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DL{tag, depth, cap, raw, gens}, m)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_value(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Get{h}, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DL{tag, depth, cap, raw, gens}, m))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, T>)}

template get_s source · line 30 · raw

@-T:Data -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T> -> @m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.get_ready(T, h, (s, m)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_value(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Get{h}, (s, m))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, T>)}

template get_r source · line 35 · raw

@-T:Data -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.get_ready(T, h, r) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_value(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Get{h}, r)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, T>)}

template set_m source · line 40 · raw

@-T:Data -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+tag:U32 -> @+depth:Nat -> @+cap:U32 -> @raw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DList<T> -> @gens:Array<U32> -> @m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.set_ready(T, h, x, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DL{tag, depth, cap, raw, gens}, m)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_unit(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Set{h, x}, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DL{tag, depth, cap, raw, gens}, m))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, Unit>)}

template set_s source · line 47 · raw

@-T:Data -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T> -> @m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.set_ready(T, h, x, (s, m)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_unit(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Set{h, x}, (s, m))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, Unit>)}

template set_r source · line 52 · raw

@-T:Data -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.set_ready(T, h, x, r) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_unit(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Set{h, x}, r)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, Unit>)}

template rm_m source · line 57 · raw

@-T:Data -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @+tag:U32 -> @+depth:Nat -> @+cap:U32 -> @raw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DList<T> -> @gens:Array<U32> -> @m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.remove_ready(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DL{tag, depth, cap, raw, gens}, m)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_value(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Remove{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}}, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DL{tag, depth, cap, raw, gens}, m))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, T>)}

template rm_s source · line 64 · raw

@-T:Data -> @+owner:U32 -> @+id:U32 -> @+g:U32 -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T> -> @m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.remove_ready(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}, (s, m)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_value(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Remove{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.H{owner, id, g}}, (s, m))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, T>)}

template rm_r source · line 69 · raw

@-T:Data -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.remove_ready(T, h, r) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_value(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Remove{h}, r)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, T>)}

template nx_m source · line 74 · raw

@-T:Data -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+tag:U32 -> @+depth:Nat -> @+cap:U32 -> @raw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DList<T> -> @gens:Array<U32> -> @m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.next_ready(T, h, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DL{tag, depth, cap, raw, gens}, m)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_neighbour(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Next{h}, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DL{tag, depth, cap, raw, gens}, m))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>>)}

template nx_s source · line 81 · raw

@-T:Data -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T> -> @m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.next_ready(T, h, (s, m)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_neighbour(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Next{h}, (s, m))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>>)}

template nx_r source · line 86 · raw

@-T:Data -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.next_ready(T, h, r) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_neighbour(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Next{h}, r)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>>)}

template pv_m source · line 91 · raw

@-T:Data -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+tag:U32 -> @+depth:Nat -> @+cap:U32 -> @raw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DList<T> -> @gens:Array<U32> -> @m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.prev_ready(T, h, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DL{tag, depth, cap, raw, gens}, m)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_neighbour(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Prev{h}, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DL{tag, depth, cap, raw, gens}, m))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>>)}

template pv_s source · line 98 · raw

@-T:Data -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T> -> @m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.prev_ready(T, h, (s, m)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_neighbour(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Prev{h}, (s, m))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>>)}

template pv_r source · line 103 · raw

@-T:Data -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.prev_ready(T, h, r) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_neighbour(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Prev{h}, r)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>>)}

template ib_m source · line 108 · raw

@-T:Data -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+tag:U32 -> @+depth:Nat -> @+cap:U32 -> @raw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DList<T> -> @gens:Array<U32> -> @m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.insert_before_ready(T, h, x, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DL{tag, depth, cap, raw, gens}, m)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_insert(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertBefore{h, x}, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DL{tag, depth, cap, raw, gens}, m))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>)}

template ib_s source · line 115 · raw

@-T:Data -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T> -> @m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.insert_before_ready(T, h, x, (s, m)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_insert(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertBefore{h, x}, (s, m))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>)}

template ib_r source · line 120 · raw

@-T:Data -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.insert_before_ready(T, h, x, r) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_insert(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertBefore{h, x}, r)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>)}

template ia_m source · line 125 · raw

@-T:Data -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @+tag:U32 -> @+depth:Nat -> @+cap:U32 -> @raw:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DList<T> -> @gens:Array<U32> -> @m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.insert_after_ready(T, h, x, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DL{tag, depth, cap, raw, gens}, m)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_insert(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertAfter{h, x}, (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DL{tag, depth, cap, raw, gens}, m))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>)}

template ia_s source · line 132 · raw

@-T:Data -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T> -> @m:Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.insert_after_ready(T, h, x, (s, m)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_insert(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertAfter{h, x}, (s, m))) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>)}

template ia_r source · line 137 · raw

@-T:Data -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error>) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.insert_after_ready(T, h, x, r) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_insert(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.checked(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertAfter{h, x}, r)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>)}

template get_step source · line 144 · raw

@-T:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.get(T, s, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_value(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Get{h})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, T>)}

template set_step source · line 147 · raw

@-T:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.set(T, s, h, x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_unit(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Set{h, x})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, Unit>)}

template remove_step source · line 150 · raw

@-T:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.remove(T, s, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_value(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Remove{h})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, T>)}

template next_step source · line 153 · raw

@-T:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.next(T, s, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_neighbour(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Next{h})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>>)}

template prev_step source · line 156 · raw

@-T:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.prev(T, s, h) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_neighbour(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Prev{h})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>>)}

template before_step source · line 159 · raw

@-T:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.insert_before(T, s, h, x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_insert(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertBefore{h, x})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>)}

template after_step source · line 162 · raw

@-T:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T> -> @+h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> @+x:T -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.insert_after(T, s, h, x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_insert(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(T, s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.InsertAfter{h, x})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>)}