law display_mines

minebender-game@1.0.0.0 · LAWS.bend:656

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

656# LAW: "Once the game is over, no mine stays covered."
657law display_mines:
658  for w: Nat
659  for h: Nat
660  for layout: T.Grid(Bool)
661  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
662  for g: G.Game
663  for r: Reachable(w, h, layout, g)
664  for over: {G.status(g) != T.Playing{} : T.Status}
665  for q: T.Pos
666  for on: {on_board(w, h, q) == True{} : Bool}
667  for m: {mine(layout, q) == True{} : Bool}
668  {is_covered(tile(g, q)) == False{} : Bool}