~/bend-docscommunity

proofs/containers/stack/components.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/stack/components.bend as Components

5 imports
import Base
import ./proof.bend as P
import ../../../src/containers/stack.bend as D
import ../../../spec/containers/stack.bend as S
import ../../../src/containers/types/stack.bend as E

Definitions

def step_u32 source · line 7 · raw

@+xs:List<&2, U32> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/stack.Op<U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/stack.step(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/stack/proof.real(U32, xs), op) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/stack/proof.lift(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/stack.step(U32, xs, op)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/stack.Stack<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/stack.Obs<U32>)}

def step_string source · line 10 · raw

@+xs:List<&2, String> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/stack.Op<String> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/stack.step(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/stack/proof.real(String, xs), op) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/stack/proof.lift(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/stack.step(String, xs, op)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/stack.Stack<String>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/stack.Obs<String>)}

def new_u32 source · line 13 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/stack.new(U32) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/stack/proof.real(U32, []) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/stack.Stack<U32>}

def new_string source · line 16 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/stack.new(String) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/stack/proof.real(String, []) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/stack.Stack<String>}