law open_mine

minebender-game@1.0.0.0 · LAWS.bend:341

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

341# LAW: "Revealing a mine loses, naming that mine, and shows it as Boom."
342law open_mine:
343  for w: Nat
344  for h: Nat
345  for layout: T.Grid(Bool)
346  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
347  for g: G.Game
348  for r: Reachable(w, h, layout, g)
349  for playing: {G.status(g) == T.Playing{} : T.Status}
350  for p: T.Pos
351  for boom: {mine(layout, p) == True{} : Bool}
352  {G.status(G.open(g, p)) == T.Lost{T.Exploded{p}} : T.Status} &
353  {seen(G.knowledge(G.open(g, p)), p) == T.Boom{} : T.Seen}