law open_over

minebender-game@1.0.0.0 · PROOF.bend:45

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

45# In a finished game, opening a cell changes nothing.
46law open_over:
47  for +g: G.Game
48  for +p: T.Pos
49  for +over: {G.is_playing(G.status(g)) == False{} : Bool}
50  {G.open(g, p) == g : G.Game}