proofs/containers/stack/components.bend

bend-collections-laws-containers@1.0.0.0 · 17 lines · 0 definitions

1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/containers/stack/proof.bend as P
3import bend-collections-laws-containers@1.0.0.0/src/containers/stack.bend as D
4import bend-collections-laws-containers@1.0.0.0/spec/containers/stack.bend as S
5import bend-collections-laws-containers@1.0.0.0/src/containers/types/stack.bend as E
6
7def step_u32(+xs: List<&2, U32>, +op: E.Op<U32>) -> {D.step(~U32, P.real(~U32, xs), op) == P.lift(~U32, S.step(U32, xs, op)) : D.Stack<U32> & E.Obs<U32>}:
8  P.step_correct(~U32, xs, op)
9
10def step_string(+xs: List<&2, String>, +op: E.Op<String>) -> {D.step(~String, P.real(~String, xs), op) == P.lift(~String, S.step(String, xs, op)) : D.Stack<String> & E.Obs<String>}:
11  P.step_correct(~String, xs, op)
12
13def new_u32() -> {D.new(~U32) == P.real(~U32, Nil{}) : D.Stack<U32>}:
14  P.constructor(~U32)
15
16def new_string() -> {D.new(~String) == P.real(~String, Nil{}) : D.Stack<String>}:
17  P.constructor(~String)