~/bend-docscommunity

proofs/containers/simple_queue/proof.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/simple_queue/proof.bend as Proof

6 imports
import Base
import ../../../src/containers/simple_queue.bend as P1
import ../../../src/containers/queue.bend as K1
import ../../../src/containers/types/queue.bend as E1
import ../../../spec/containers/simple_queue.bend as S
import ../queue/proof.bend as UP

Definitions

def simple_queue_put source · line 10 · raw

@q:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<U32> -> @+v:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/simple_queue.put(U32, q, v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.enqueue(U32, q, v) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<U32>}

def simple_queue_get source · line 13 · raw

@q:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/simple_queue.get(U32, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.dequeue(U32, q) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Error, U32>)}

def simple_queue_qsize source · line 16 · raw

@q:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/simple_queue.qsize(U32, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.length(U32, q) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<U32>, Nat)}

def length_result source · line 41 · raw

@-T:Data -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/simple_queue.Length.length_result(T, xs)

def length_frame source · line 44 · raw

@-T:Data -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/simple_queue.Length.length_frame(T, xs)

def to_list_model source · line 47 · raw

@-T:Data -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/simple_queue.Iteration.to_list_model(T, xs)

def to_list_frame source · line 50 · raw

@-T:Data -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/simple_queue.Iteration.to_list_frame(T, xs)

def enqueue_length source · line 53 · raw

@-T:Data -> @+xs:List<&2, T> -> @+v:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/simple_queue.Append.enqueue_length(T, xs, v)

def enqueue_prefix source · line 56 · raw

@-T:Data -> @+xs:List<&2, T> -> @+v:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/simple_queue.Append.enqueue_prefix(T, xs, v)

def enqueue_element source · line 59 · raw

@-T:Data -> @+xs:List<&2, T> -> @+v:T -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/simple_queue.Append.enqueue_element(T, xs, v)

def dequeue_length source · line 62 · raw

@-T:Data -> @+h:T -> @+t:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/simple_queue.Delete_First.dequeue_length(T, h, t)

def dequeue_shifted source · line 65 · raw

@-T:Data -> @+h:T -> @+t:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/simple_queue.Delete_First.dequeue_shifted(T, h, t)

def dequeue_result source · line 68 · raw

@-T:Data -> @+h:T -> @+t:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/simple_queue.Delete_First.dequeue_result(T, h, t)

def dequeue_empty source · line 71 · raw

@-T:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/simple_queue.Delete_First.dequeue_empty(T)

def peek_first source · line 74 · raw

@-T:Data -> @+h:T -> @+t:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/simple_queue.First_Element.peek_first(T, h, t)

def peek_frame source · line 77 · raw

@-T:Data -> @+xs:List<&2, T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/simple_queue.First_Element.peek_frame(T, xs)

def peek_empty source · line 80 · raw

@-T:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/simple_queue.First_Element.peek_empty(T)

Templates

template new_is source · line 21 · raw

@-T:Data -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/simple_queue.new(T) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.new(T) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<T>}

template qsize_is source · line 24 · raw

@-T:Data -> @q:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<T> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/simple_queue.qsize(T, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.length(T, q) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<T>, Nat)}

template put_is source · line 27 · raw

@-T:Data -> @q:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<T> -> @x:T -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/simple_queue.put(T, q, x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.enqueue(T, q, x) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<T>}

template get_is source · line 30 · raw

@-T:Data -> @q:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<T> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/simple_queue.get(T, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.dequeue(T, q) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Error, T>)}

template peek_is source · line 33 · raw

@-T:Data -> @q:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<T> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/simple_queue.peek(T, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.peek(T, q) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Error, T>)}

template to_list_is source · line 36 · raw

@-T:Data -> @q:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<T> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/simple_queue.to_list(T, q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.to_list(T, q) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<T>, List<&2, T>)}