law display_play

minebender-game@1.0.0.0 · LAWS.bend:615

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

615# LAW: "During play, the screen shows exactly what the player knows, and
616# their flags": nothing about the hidden mines leaks onto the screen.
617law display_play:
618  for w: Nat
619  for h: Nat
620  for layout: T.Grid(Bool)
621  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
622  for g: G.Game
623  for r: Reachable(w, h, layout, g)
624  for playing: {G.status(g) == T.Playing{} : T.Status}
625  for p: T.Pos
626  for on: {on_board(w, h, p) == True{} : Bool}
627  {tile(g, p) == tile_of(seen(G.knowledge(g), p), G.flagged(g, p)) : T.Tile}