ProofSolver.solve_stuck.go: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_solver.bend as ProofSolver
Lines 2821-2841 of minebender-game@1.0.0.0/proof_solver.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_solver.bend&start_line=2821&end_line=2841

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

def solve_stuck.go(+w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +ok: Bool,
  oke: {B.shaped(T.Seen, w, h, rows) == ok : Bool},
  e: {S.solve.go(ok, S.hidden_cells(rows, B.cells(w, h)), w, h, n, rows) == None{} : Maybe<&2, T.Pos>},
  +p: T.Pos, ps: L.ProvablySafe(T.Knowledge{w, h, n, rows}, p)) -> Empty:
  match ok:
    case False{}:
      match ps:
        case (+hid, H):
          head_none(S.hidden_cells(rows, B.cells(w, h)), p, e,
            hc_member(rows, B.cells(w, h), p, PS.cells_member(w, h, p, hid_on(w, h, n, rows, p, hid)), hid_hp(w, h, n, rows, p, hid)))
    case True{}:
      match ps:
        case (+hid, H):
          +hs = S.hidden_cells(rows, B.cells(w, h))
          +its = S.items(w, h, rows, B.cells(w, h))
          +shS = Equal.trans(Bool, B.shaped(Maybe<&2, Bool>, w, h, S.start(rows)), B.shaped(T.Seen, w, h, rows), True{},
            start_shaped(w, h, rows), oke)
          +mp = hc_member(rows, B.cells(w, h), p, PS.cells_member(w, h, p, hid_on(w, h, n, rows, p, hid)), hid_hp(w, h, n, rows, p, hid))
          stuck_wit(w, h, n, rows, p, H,
            loop_none(hs, Nil{}, S.plan(w, h, S.todos(its, hs)), S.start(rows), w, h, n, rows, its, e, {==}, shS,
              hc_on(rows, w, h, B.cells(w, h), PS.cells_on(w, h)), p, mp))

Uses (30):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=ProvablySafe
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=cells
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=shaped
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=cells_member
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=cells_on
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=hc_member
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=hc_on
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=head_none
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=hid_hp
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=hid_on
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=loop_none
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=start_shaped
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=stuck_wit
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=hidden_cells
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=items
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=plan
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=solve.go
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=start
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=todos
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Grid
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Knowledge
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Seen