law neighbours_member

minebender-game@1.0.0.0 · proof_cells.bend:461

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

461# An adjacent cell of the board is a neighbour.
462law neighbours_member:
463  for +w: Nat
464  for +h: Nat
465  for +s: T.Pos
466  for +r: T.Pos
467  for on: {B.on_board(w, h, r) == True{} : Bool}
468  for a: {B.adjacent(s, r) == True{} : Bool}
469  {B.contains(B.neighbours(w, h, s), r) == True{} : Bool}