law bridge

minebender-game@1.0.0.0 · LAWS.bend:293

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

293# LAW: "The real board is always consistent with what the player sees."
294# Without it, the knowledge laws below would say nothing about the real game.
295# It also covers "every number equals its count of adjacent mines".
296law bridge:
297  for w: Nat
298  for h: Nat
299  for layout: T.Grid(Bool)
300  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
301  for g: G.Game
302  for r: Reachable(w, h, layout, g)
303  {consistent(G.knowledge(g), layout) == True{} : Bool}