law at_set_ne

minebender-game@1.0.0.0 · proof_lists.bend:311

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

311# Setting p leaves every other cell as it was.
312law at_set_ne:
313  for -A: Data
314  for +g: T.Grid(A)
315  for +p: T.Pos
316  for +q: T.Pos
317  for +v: A
318  for +d: A
319  for ne: {B.same(p, q) == False{} : Bool}
320  {B.at(A, d, B.set_at(A, g, p, v), q) == B.at(A, d, g, q) : A}