def closed_use.go

minebender-game@1.0.0.0 · proof_inv.bend:38

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

38def closed_use.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: T.Grid(Bool), +q: T.Pos, +r: T.Pos,
39  f: {Bool.or(Bool.not(Bool.and(True{}, True{})),
40    PS.allp(~T.Grid(Bool), ~shown_in, g, B.neighbours(w, h, q))) == True{} : Bool},
41  rm: {B.contains(B.neighbours(w, h, q), r) == True{} : Bool}) ->
42  {B.at(Bool, False{}, g, r) == True{} : Bool}:
43  PS.allp_member(~T.Grid(Bool), ~shown_in, g, B.neighbours(w, h, q), r, f, rm)