def Inv

minebender-game@1.0.0.0 · proof_inv.bend:481

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

481# What every real game satisfies: the board it was started with, a grid of
482# revealed cells of the board's shape, Won exactly when every safe cell is
483# revealed, no revealed mine during play, and every revealed zero's
484# neighbours revealed.
485def Inv(+w: Nat, +h: Nat, +layout: T.Grid(Bool), g: G.Game) -> Type:
486  match g:
487    case G.Game{gw, gh, gl, shown, flags, status}:
488      {gw == w : Nat} & ({gh == h : Nat} & ({gl == layout : T.Grid(Bool)} & Facts(w, h, layout, shown, status)))