law display_blast

minebender-game@1.0.0.0 · LAWS.bend:629

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

629# LAW: "After an explosion, the screen shows the mine that exploded."
630law display_blast:
631  for w: Nat
632  for h: Nat
633  for layout: T.Grid(Bool)
634  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
635  for g: G.Game
636  for r: Reachable(w, h, layout, g)
637  for p: T.Pos
638  for lost: {G.status(g) == T.Lost{T.Exploded{p}} : T.Status}
639  for on: {on_board(w, h, p) == True{} : Bool}
640  {tile(g, p) == T.Blast{} : T.Tile}