law flag_toggle

minebender-game@1.0.0.0 · LAWS.bend:436

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

436# LAW: "Flagging a hidden cell during play toggles its flag."
437law flag_toggle:
438  for g: G.Game
439  for playing: {G.status(g) == T.Playing{} : T.Status}
440  for p: T.Pos
441  for hid: {hidden(G.knowledge(g), p) == True{} : Bool}
442  {G.flagged(G.step(g, T.Flag{p}), p) == Bool.not(G.flagged(g, p)) : Bool}