proofs/containers/queue/state.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/queue/state.bend as State

3 imports

import Base
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/queue.bend as Q

Types

type Shadow source · line 9 · raw

@-T:Data -> Data

Sh

@-T:Data -> @front:List<&2, T> -> @back:List<&2, T> -> Shadow<T>

Definitions

def initial source · line 12 · raw

@-T:Data -> Shadow<T>

def real source · line 15 · raw

@-T:Data -> @sh:Shadow<T> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<T>

def model source · line 20 · raw

@-T:Data -> @sh:Shadow<T> -> List<&2, T>

def unreal source · line 25 · raw

@-T:Data -> @q:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<T> -> Shadow<T>

def unreal_real source · line 29 · raw

@-T:Data -> @+sh:Shadow<T> -> {unreal(T, real(T, sh)) == sh : Shadow<T>}

def real_inj source · line 35 · raw

@-T:Data -> @+a:Shadow<T> -> @+b:Shadow<T> -> @+e:{real(T, a) == real(T, b) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<T>} -> {a == b : Shadow<T>}

a queue determines its shadow