law run_step

bend-lawful-stdlib@0.1.0.0 · src/sim.bend:63

import Base
import bend-lawful-stdlib@0.1.0.0/src/class.bend as C

63# run's last step is its outermost one
64law run_step:
65  for ~P: Data
66  for ~g: C.Group<P>
67  for ~F: P -> P
68  for k: Nat
69  for s: State<P>
70  {step(~P, ~g, ~F, run(~P, ~g, ~F, k, s)) == run(~P, ~g, ~F, k, step(~P, ~g, ~F, s)) : State<P>}