law gen_count

minebender-game@1.0.0.0 · LAWS.bend:556

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

556# LAW: "Generated boards have exactly n mines" (when they fit beside the first
557# click).
558law gen_count:
559  for w: Nat
560  for h: Nat
561  for n: Nat
562  for first: T.Pos
563  for rs: List<&2, U32>
564  for on: {on_board(w, h, first) == True{} : Bool}
565  for fits: {Nat.is_lt(n, Nat.mul(w, h)) == True{} : Bool}
566  {total_mines(G.place_mines(w, h, n, first, rs)) == n : Nat}