law display_hint

minebender-game@1.0.0.0 · LAWS.bend:642

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

642# LAW: "After the assist is pressed too early, the screen shows the safe cell
643# the player could have revealed."
644law display_hint:
645  for w: Nat
646  for h: Nat
647  for layout: T.Grid(Bool)
648  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
649  for g: G.Game
650  for r: Reachable(w, h, layout, g)
651  for s: T.Pos
652  for lost: {G.status(g) == T.Lost{T.AssistTooEarly{s}} : T.Status}
653  for on: {on_board(w, h, s) == True{} : Bool}
654  {tile(g, s) == T.Hint{} : T.Tile}