def Canon

minebender-game@1.0.0.0 · proof_laws.bend:28

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

28def Canon(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game) -> Type:
29  {g == G.Game{w, h, layout, shown_of(g), flags_of(g), G.status(g)} : G.Game} &
30  PI.Facts(w, h, layout, shown_of(g), G.status(g))