ProofSolver.loop_some.cov: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_solver.bend as ProofSolver
Lines 2257-2269 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=2257&end_line=2269

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/solver.bend as S

def loop_some.cov(+c0: T.Pos, +t: List<&2, T.Pos>, +found: List<&2, T.Grid(Bool)>, +todo: S.Plan,
  +part: T.Grid(Maybe<&2, Bool>), +ctx: S.Ctx, +c: T.Pos, +b: Bool,
  e: {S.loop.if(b, u => S.loop(t, found, todo, part, ctx),
      v => S.loop.found(S.search(c0, todo, part, ctx), c0, l => S.loop(t, l <> found, todo, part, ctx))) == Some{c} : Maybe<&2, T.Pos>},
  ihf: {S.loop(t, found, todo, part, ctx) == Some{c} : Maybe<&2, T.Pos>} -> LoopSome(t, todo, part, ctx, c),
  ihn: @l: T.Grid(Bool) -> {S.loop(t, l <> found, todo, part, ctx) == Some{c} : Maybe<&2, T.Pos>} -> LoopSome(t, todo, part, ctx, c)) ->
  LoopSome(c0 <> t, todo, part, ctx, c):
  match b:
    case True{}:
      loop_some.lift(c0, t, todo, part, ctx, c, ihf(e))
    case False{}:
      loop_some.found(c0, t, found, todo, part, ctx, c,
        loop_found_some(S.search(c0, todo, part, ctx), c0, l => S.loop(t, l <> found, todo, part, ctx), c, e), ihn)

Uses (15):
  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/proof_solver.bend&name=LoopSome
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=loop_found_some
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=loop_some.found
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=loop_some.lift
  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=Plan
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=loop
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=loop.found
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=loop.if
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=search
  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