law mine_on

minebender-game@1.0.0.0 · proof_laws.bend:605

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

605# A mine of a w-by-h layout is on the board.
606law mine_on:
607  for +w: Nat
608  for +h: Nat
609  for +layout: T.Grid(Bool)
610  for +sh: {B.shaped(Bool, w, h, layout) == True{} : Bool}
611  for +p: T.Pos
612  for m: {B.mine(layout, p) == True{} : Bool}
613  {B.on_board(w, h, p) == True{} : Bool}