def safe_hidden

minebender-game@1.0.0.0 · proof_solver.bend:2752

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/solver.bend as S
import minebender-game@1.0.0.0/LAWS.bend as L
import minebender-game@1.0.0.0/proof_cells.bend as PS

2752def safe_hidden(+w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +c: T.Pos,
2753  hc: {S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, c)) == True{} : Bool} & {B.contains(B.cells(w, h), c) == True{} : Bool},
2754  fn: @layout: T.Grid(Bool) -> {L.consistent(T.Knowledge{w, h, n, rows}, layout) == True{} : Bool} -> {L.mine(layout, c) == False{} : Bool}) ->
2755  L.ProvablySafe(T.Knowledge{w, h, n, rows}, c):
2756  match hc:
2757    case (hp, mc):
2758      (hid_to(w, h, n, rows, c, PS.allp_member(~PS.WH, ~PS.onb, PS.WH{w, h}, B.cells(w, h), c, PS.cells_on(w, h), mc), hp), fn)