law reveal_flagged

minebender-game@1.0.0.0 · LAWS.bend:403

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

403# LAW: "Clicking a flagged cell does nothing."
404law reveal_flagged:
405  for g: G.Game
406  for p: T.Pos
407  for flag: {G.flagged(g, p) == True{} : Bool}
408  {G.step(g, T.Reveal{p}) == g : G.Game}