law gen_opening

minebender-game@1.0.0.0 · LAWS.bend:577

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

577# LAW: "When there's room, the first click opens an area: no mine on it or
578# next to it." (As in Windows Vista and later.)
579law gen_opening:
580  for w: Nat
581  for h: Nat
582  for n: Nat
583  for first: T.Pos
584  for rs: List<&2, U32>
585  for room: {Nat.is_le(Nat.add(n, 9n), Nat.mul(w, h)) == True{} : Bool}
586  for q: T.Pos
587  for near: {within_one(first, q) == True{} : Bool}
588  {mine(G.place_mines(w, h, n, first, rs), q) == False{} : Bool}