~/bend-docscommunity

proofs/containers/doubly_linked_list/direct_laws.bend checks

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

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/doubly_linked_list.bend as E
import ../../../src/containers/types/internal_dlist.bend as I

Definitions

def get_u32 source · line 22 · raw

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

def get_string source · line 25 · raw

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

def set_u32 source · line 43 · raw

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

def set_string source · line 46 · raw

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

def length_result_same source · line 49 · raw

@tag:U32 -> @depth:Nat -> @cap:U32 -> @gens:Array<U32> -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DList<U32>, Nat) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.length_direct_result(U32, tag, depth, cap, gens, r) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_length(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.length_result(U32, tag, depth, cap, gens, r)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32>, Nat)}

def length_same source · line 54 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.length(U32, s) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_length(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(U32, s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Length{})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32>, Nat)}

def to_list_result_same source · line 59 · raw

@tag:U32 -> @depth:Nat -> @cap:U32 -> @gens:Array<U32> -> @r:Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/internal/dlist_storage.DList<U32>, List<&2, U32>) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.to_list_direct_result(U32, tag, depth, cap, gens, r) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_list(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.list_result(U32, tag, depth, cap, gens, r)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32>, List<&2, U32>)}

def to_list_same source · line 64 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.to_list(U32, s) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_list(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.step(U32, s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.ToList{})) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32>, List<&2, U32>)}

def next_U32 source · line 76 · raw

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

def next_String source · line 79 · raw

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

def prev_U32 source · line 89 · raw

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

def prev_String source · line 92 · raw

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

def insert_before_U32 source · line 102 · raw

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

def insert_before_String source · line 105 · raw

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

def insert_after_U32 source · line 115 · raw

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

def insert_after_String source · line 118 · raw

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

def remove_U32 source · line 128 · raw

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

def remove_String source · line 131 · raw

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

Templates

template result_same source · line 7 · raw

@-T:Data -> @tag:U32 -> @depth:Nat -> @cap:U32 -> @gens:Array<U32> -> @r: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, r) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_value(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.value_result(T, tag, depth, cap, gens, r)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, T>)}

template ready_same source · line 12 · 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 get_same source · line 19 · 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_result_same source · line 28 · raw

@-T:Data -> @tag:U32 -> @depth:Nat -> @cap:U32 -> @gens:Array<U32> -> @r: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, r) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.project_unit(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.unit_result(T, tag, depth, cap, gens, r)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, Unit>)}

template set_ready_same source · line 33 · 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 set_same source · line 40 · 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 next_ready_same 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.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 prev_ready_same source · line 82 · 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 insert_before_ready_same source · line 95 · 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 insert_after_ready_same source · line 108 · 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 remove_ready_same source · line 121 · 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>)}