law run_inv

bend-lawful-stdlib@0.1.0.0 · src/machine.bend:16

import Base

16# a step that keeps Inv keeps it over any input list
17law run_inv:
18  for ~S: Data
19  for ~I: Data
20  for ~step: S -> I -> S
21  for ~Inv: S -> Type
22  for ~keep: @s: S -> @i: I -> Inv(s) -> Inv(step(s, i))
23  for xs: List<&2, I>
24  for +s: S
25  Inv(s) -> Inv(run(~S, ~I, ~step, s, xs))