law flag_others

minebender-game@1.0.0.0 · LAWS.bend:444

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

444# LAW: "Flagging p leaves every other cell's flag alone."
445law flag_others:
446  for g: G.Game
447  for p: T.Pos
448  for q: T.Pos
449  for diff: {p != q : T.Pos}
450  {G.flagged(G.step(g, T.Flag{p}), q) == G.flagged(g, q) : Bool}