law zero_nbr

minebender-game@1.0.0.0 · proof_cells.bend:598

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

598# The neighbours of a zero have no mines.
599law zero_nbr:
600  for +w: Nat
601  for +h: Nat
602  for +layout: T.Grid(Bool)
603  for +s: T.Pos
604  for +r: T.Pos
605  for z: {B.zero(w, h, layout, s) == True{} : Bool}
606  for m: {B.contains(B.neighbours(w, h, s), r) == True{} : Bool}
607  {B.mine(layout, r) == False{} : Bool}