law flag_no_knowledge

minebender-game@1.0.0.0 · LAWS.bend:428

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

428# LAW: "Flags are not knowledge": flagging changes neither what the player
429# sees nor the game's status.
430law flag_no_knowledge:
431  for g: G.Game
432  for p: T.Pos
433  {G.knowledge(G.step(g, T.Flag{p})) == G.knowledge(g) : T.Knowledge} &
434  {G.status(G.step(g, T.Flag{p})) == G.status(g) : T.Status}