law play_cell

minebender-game@1.0.0.0 · proof_display.bend:101

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

101law play_cell:
102  for +c: Bool
103  for +m: Bool
104  for +fl: Bool
105  for +w: Nat
106  for +h: Nat
107  for +layout: T.Grid(Bool)
108  for +p: T.Pos
109  {G.tile.go(None{}, c, m, fl, T.Playing{}, w, h, layout, p)
110    == L.tile_of(G.seen_pick(c, m, w, h, layout, p), Bool.and(Bool.and(True{}, Bool.not(c)), fl)) : T.Tile}