def safe_hidden.k

minebender-game@1.0.0.0 · proof_solver.bend:2760

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

2760def safe_hidden.k(+w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +c: T.Pos,
2761  hc: {S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, c)) == True{} : Bool} & {B.contains(B.cells(w, h), c) == True{} : Bool},
2762  fn: {B.on_board(w, h, c) == True{} : Bool} ->
2763    @layout: T.Grid(Bool) -> {L.consistent(T.Knowledge{w, h, n, rows}, layout) == True{} : Bool} -> {L.mine(layout, c) == False{} : Bool}) ->
2764  L.ProvablySafe(T.Knowledge{w, h, n, rows}, c):
2765  match hc:
2766    case (hp, mc):
2767      +onc = PS.allp_member(~PS.WH, ~PS.onb, PS.WH{w, h}, B.cells(w, h), c, PS.cells_on(w, h), mc)
2768      (hid_to(w, h, n, rows, c, onc, hp), fn(onc))