law canon

minebender-game@1.0.0.0 · proof_laws.bend:32

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/game.bend as G
import minebender-game@1.0.0.0/proof_inv.bend as PI

32# A real game in its canonical form, with the facts of the invariant.
33law canon:
34  for +w: Nat
35  for +h: Nat
36  for +layout: T.Grid(Bool)
37  for +g: G.Game
38  for inv: PI.Inv(w, h, layout, g)
39  Canon(w, h, layout, g)