law count_zero_member

minebender-game@1.0.0.0 · proof_cells.bend:578

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

578# A list with no mines has no mine on any of its cells.
579law count_zero_member:
580  for +layout: T.Grid(Bool)
581  for +ns: List<&2, T.Pos>
582  for +r: T.Pos
583  for +z: {B.count_mines(layout, ns) == 0n : Nat}
584  for m: {B.contains(ns, r) == True{} : Bool}
585  {B.mine(layout, r) == False{} : Bool}