~/bend-docscommunity

src/machine.bend checks

raw source on the hub · import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/machine.bend as Machine

1 import
import Base

Laws

law run_inv provedsource · line 17 · raw

@-S:Data -> @-I:Data -> @-step:(@_:S -> @_:I -> S) -> @-Inv:(@_:S -> Type) -> @-keep:(@s:S -> @i:I -> @_:Inv(s) -> Inv(step(s, i))) -> @xs:List<&2, I> -> @+s:S -> @_:Inv(s) -> Inv(run(S, I, step, s, xs))

a step that keeps Inv keeps it over any input list

Templates

template run source · line 13 · raw

@-S:Data -> @-I:Data -> @-step:(@_:S -> @_:I -> S) -> @s:S -> @xs:List<&2, I> -> S