law gen_first_safe

minebender-game@1.0.0.0 · LAWS.bend:568

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

568# LAW: "The first click is safe."
569law gen_first_safe:
570  for w: Nat
571  for h: Nat
572  for n: Nat
573  for first: T.Pos
574  for rs: List<&2, U32>
575  {mine(G.place_mines(w, h, n, first, rs), first) == False{} : Bool}