ProofInv.Inv: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_inv.bend as ProofInv
Lines 481-488 of minebender-game@1.0.0.0/proof_inv.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_inv.bend&start_line=481&end_line=488

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

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

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=Game
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_inv.bend&name=Facts
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Grid