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

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

def dfs_some_keep.node(+c: T.Pos, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +part: T.Grid(Maybe<&2, Bool>),
  +ctx: S.Ctx, +l: T.Grid(Bool), +q: T.Pos, +bq: Bool, +fr: Bool, +fre: {S.is_none(S.look(part, c)) == fr : Bool},
  e: {S.dfs.free(fr, u => S.dfs(rest, part, ctx),
      v => S.dfs.or(S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel, S.ctx_n(ctx)),
        x => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), ctx)),
      y => S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel, S.ctx_n(ctx)),
        z => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), ctx)))) == Some{l} : Maybe<&2, T.Grid(Bool)>},
  +lq: {S.look(part, q) == Some{bq} : Maybe<&2, Bool>},
  kp: {S.dfs(rest, part, ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} -> {B.mine(l, q) == bq : Bool},
  k0: {S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} ->
    {S.look(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), q) == Some{bq} : Maybe<&2, Bool>} -> {B.mine(l, q) == bq : Bool},
  k1: {S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} ->
    {S.look(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), q) == Some{bq} : Maybe<&2, Bool>} -> {B.mine(l, q) == bq : Bool}) ->
  {B.mine(l, q) == bq : Bool}:
  match fr:
    case False{}:
      kp(e)
    case True{}:
      +d0 = S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), ctx)
      +d1 = S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), ctx)
      dfs_some_keep.br(l, q, bq, d0, d1,
        dfs_branch_some(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel, S.ctx_n(ctx)),
          S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel, S.ctx_n(ctx)), d0, d1, l, e),
        e0 => k0(e0, set_keep(part, c, q, Some{False{}}, bq, fre, lq, B.same(c, q), {==})),
        e1 => k1(e1, set_keep(part, c, q, Some{True{}}, bq, fre, lq, B.same(c, q), {==})))

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=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=same
  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/proof_solver.bend&name=dfs_branch_some
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=dfs_some_keep.br
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=set_keep
  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=ctx_n
  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=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