law won_iff

minebender-game@1.0.0.0 · LAWS.bend:305

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

305# LAW: "The game is won exactly when every safe cell is revealed."
306law won_iff:
307  for w: Nat
308  for h: Nat
309  for layout: T.Grid(Bool)
310  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
311  for g: G.Game
312  for r: Reachable(w, h, layout, g)
313  {is_won(G.status(g)) == all_safe_revealed(G.knowledge(g), layout) : Bool}