law gen_shape

minebender-game@1.0.0.0 · LAWS.bend:547

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

547# LAW: "Generated boards have the requested shape."
548law gen_shape:
549  for w: Nat
550  for h: Nat
551  for n: Nat
552  for first: T.Pos
553  for rs: List<&2, U32>
554  {shaped(Bool, w, h, G.place_mines(w, h, n, first, rs)) == True{} : Bool}