~/bend-docscommunity

src/queue.bend checks

raw source on the hub · import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/queue.bend as Queue

2 imports
import Base
import ./list.bend as List

Laws

law push_model provedsource · line 56 · raw

@-A:Data -> @q:Queue<A> -> @+x:A -> {List.append(&2, A, model(A, q), [x]) == model(A, push(A, q, x)) : List<&2, A>}

push appends x to the model.

law pop_model.rot provedsource · line 71 · raw

@-A:Data -> @f:List<&2, A> -> {0x5f97f469d15c04a181dae0e4e64e1d3d/src/list.uncons(A, f) == pop.model(A, pop.rot(A, f)) : 0x5f97f469d15c04a181dae0e4e64e1d3d/src/list.Step<&2, A, List<&2, A>>}

law pop_model provedsource · line 85 · raw

@-A:Data -> @q:Queue<A> -> {0x5f97f469d15c04a181dae0e4e64e1d3d/src/list.uncons(A, model(A, q)) == pop.model(A, pop(A, q)) : 0x5f97f469d15c04a181dae0e4e64e1d3d/src/list.Step<&2, A, List<&2, A>>}

pop returns the model's head and tail.

Types

type Queue source · line 16 · raw

@-A:Data -> Type

Definitions

def empty source · line 19 · raw

@-A:Data -> Queue<A>

def model source · line 22 · raw

@-A:Data -> @q:Queue<A> -> List<&2, A>

def push source · line 27 · raw

@-A:Data -> @q:Queue<A> -> @x:A -> Queue<A>

def pop.rot source · line 33 · raw

@-A:Data -> @f:List<&2, A> -> 0x5f97f469d15c04a181dae0e4e64e1d3d/src/list.Step<&1, A, Queue<A>>

front is empty; f is the reversed rear

def pop source · line 40 · raw

@-A:Data -> @q:Queue<A> -> 0x5f97f469d15c04a181dae0e4e64e1d3d/src/list.Step<&1, A, Queue<A>>

def pop.model source · line 48 · raw

@-A:Data -> @s:0x5f97f469d15c04a181dae0e4e64e1d3d/src/list.Step<&1, A, Queue<A>> -> 0x5f97f469d15c04a181dae0e4e64e1d3d/src/list.Step<&2, A, List<&2, A>>

pop's result with the remaining queue replaced by its model