ProofSolver.dfs_none.node: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_solver.bend as ProofSolver
Lines 975-1000 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=975&end_line=1000

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/proof_cells.bend as PS

def dfs_none.node(+c: T.Pos, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +part: T.Grid(Maybe<&2, Bool>),
  +w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +its: List<&2, S.Item>, +layout: T.Grid(Bool),
  +shP: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}, +shL: {B.shaped(Bool, w, h, layout) == True{} : Bool},
  +cov: {covers(w, h, S.Todo{c, rel} <> rest, part) == True{} : Bool},
  +comp: {completes(w, h, part, layout) == True{} : Bool}, +tot: {B.total_mines(layout) == n : Nat},
  +rok: {S.items_ok(rel, layout) == True{} : Bool}, +ron: {items_onb(PS.WH{w, h}, rel) == True{} : Bool},
  +fr: Bool, fre: {S.is_none(S.look(part, c)) == fr : Bool},
  e: {S.dfs.free(fr, u => S.dfs(rest, part, S.Ctx{w, h, n, rows, its}),
      v => S.dfs.or(S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel, n),
        x => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), S.Ctx{w, h, n, rows, its})),
      y => S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel, n),
        z => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), S.Ctx{w, h, n, rows, its})))) == None{} : Maybe<&2, T.Grid(Bool)>},
  kp: {S.dfs(rest, part, S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Grid(Bool)>} ->
    {covers(w, h, rest, part) == True{} : Bool} -> Empty,
  k0: {S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Grid(Bool)>} ->
    {covers(w, h, rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}})) == True{} : Bool} ->
    {completes(w, h, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), layout) == True{} : Bool} -> Empty,
  k1: {S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Grid(Bool)>} ->
    {covers(w, h, rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}})) == True{} : Bool} ->
    {completes(w, h, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), layout) == True{} : Bool} -> Empty) -> Empty:
  match fr:
    case False{}:
      kp(e, covers_skip(c, rel, rest, part, fre, B.cells(w, h), cov))
    case True{}:
      dfs_none.pick(c, rel, rest, part, w, h, n, rows, its, layout, shP, shL, cov, comp, tot, rok, ron,
        B.mine(layout, c), {==}, e, k0, k1)

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=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=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=mine
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=set_at
  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/board.bend&name=total_mines
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=WH
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=completes
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=covers
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=covers_skip
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=dfs_none.pick
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=items_onb
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=Ctx
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=Item
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=Todo
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=dfs
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=dfs.free
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=dfs.or
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=dfs.when
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=is_none
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=items_ok
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=look
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=open_ok
  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=Pos
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Seen