law display_mines_c

minebender-game@1.0.0.0 · proof_display.bend:266

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/board.bend as B
import minebender-game@1.0.0.0/game.bend as G
import minebender-game@1.0.0.0/LAWS.bend as L

266law display_mines_c:
267  for +w: Nat
268  for +h: Nat
269  for +layout: T.Grid(Bool)
270  for +s: T.Grid(Bool)
271  for +f: List<&2, T.Pos>
272  for +st: T.Status
273  for over: {st != T.Playing{} : T.Status}
274  for +q: T.Pos
275  for +on: {B.on_board(w, h, q) == True{} : Bool}
276  for +m: {B.mine(layout, q) == True{} : Bool}
277  {L.is_covered(L.tile(G.Game{w, h, layout, s, f, st}, q)) == False{} : Bool}