law flags_hidden

minebender-game@1.0.0.0 · LAWS.bend:452

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

452# LAW: "Only hidden cells carry flags": revealing a flagged cell clears its
453# flag, and no cell off the board is ever flagged.
454law flags_hidden:
455  for w: Nat
456  for h: Nat
457  for layout: T.Grid(Bool)
458  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
459  for g: G.Game
460  for r: Reachable(w, h, layout, g)
461  for q: T.Pos
462  for flag: {G.flagged(g, q) == True{} : Bool}
463  {hidden(G.knowledge(g), q) == True{} : Bool}