src/sim.bend checks

raw source on the hub · import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/sim.bend as Sim

2 imports

import Base
import ./class.bend as C

Laws

law back_step provedsource · line 34 · raw

@-P:Data -> @-g:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Group<P> -> @-F:(@_:P -> P) -> @s:State<P> -> {s == back(P, g, F, step(P, g, F, s)) : State<P>}

back undoes step

law run_step provedsource · line 64 · raw

@-P:Data -> @-g:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Group<P> -> @-F:(@_:P -> P) -> @k:Nat -> @s:State<P> -> {step(P, g, F, run(P, g, F, k, s)) == run(P, g, F, k, step(P, g, F, s)) : State<P>}

run's last step is its outermost one

law rewind_run provedsource · line 80 · raw

@-P:Data -> @-g:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Group<P> -> @-F:(@_:P -> P) -> @+n:Nat -> @+s:State<P> -> {s == rewind(P, g, F, n, run(P, g, F, n, s)) : State<P>}

rewinding n steps undoes running n steps

Types

type State source · line 18 · raw

@-P:Data -> Data

State
```
@-P:Data -> @x:P -> @v:P -> State<P>
```

Templates

template step source · line 21 · raw

@-P:Data -> @-g:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Group<P> -> @-F:(@_:P -> P) -> @s:State<P> -> State<P>

template back source · line 27 · raw

@-P:Data -> @-g:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Group<P> -> @-F:(@_:P -> P) -> @s:State<P> -> State<P>

template run source · line 49 · raw

@-P:Data -> @-g:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Group<P> -> @-F:(@_:P -> P) -> @n:Nat -> @s:State<P> -> State<P>

template rewind source · line 56 · raw

@-P:Data -> @-g:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Group<P> -> @-F:(@_:P -> P) -> @n:Nat -> @s:State<P> -> State<P>