def safe_fn

minebender-game@1.0.0.0 · proof_solver.bend:2727

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_copy.bend as PC

2727def safe_fn(+w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +okt: {B.shaped(T.Seen, w, h, rows) == True{} : Bool},
2728  +c: T.Pos, +onc: {B.on_board(w, h, c) == True{} : Bool},
2729  +sn: {S.search(c, S.plan(w, h, S.todos(S.items(w, h, rows, B.cells(w, h)), S.hidden_cells(rows, B.cells(w, h)))),
2730    S.start(rows), S.Ctx{w, h, n, rows, S.items(w, h, rows, B.cells(w, h))}) == None{} : Maybe<&2, T.Grid(Bool)>},
2731  +layout: T.Grid(Bool), +cons: {L.consistent(T.Knowledge{w, h, n, rows}, layout) == True{} : Bool},
2732  +b: Bool, be: {B.mine(layout, c) == b : Bool}) -> {L.mine(layout, c) == False{} : Bool}:
2733  match b:
2734    case False{}:
2735      %PC.mine_eq(layout, c) : {_ == False{} : Bool}
2736      be
2737    case True{}:
2738      Empty.absurd({L.mine(layout, c) == False{} : Bool}, search_none(w, h, n, rows, okt, c, onc, layout, cons, be, sn))