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

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 loop_none.cov(+c0: T.Pos, +t: List<&2, T.Pos>, +found: List<&2, T.Grid(Bool)>, +todo: S.Plan,
  +part: T.Grid(Maybe<&2, Bool>), +w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +its: List<&2, S.Item>,
  +val: {all_valid(S.Ctx{w, h, n, rows, its}, found) == True{} : Bool},
  +shP: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}, on0: {B.on_board(w, h, c0) == True{} : Bool},
  +c: T.Pos, mr: Or({B.same(c0, c) == True{} : Bool}, {B.contains(t, c) == True{} : Bool}),
  +b: Bool, be: {S.covered(found, c0) == b : Bool},
  e: {S.loop.if(b, u => S.loop(t, found, todo, part, S.Ctx{w, h, n, rows, its}),
      v => S.loop.found(S.search(c0, todo, part, S.Ctx{w, h, n, rows, its}), c0,
        l => S.loop(t, l <> found, todo, part, S.Ctx{w, h, n, rows, its}))) == None{} : Maybe<&2, T.Pos>},
  ihf: {S.loop(t, found, todo, part, S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Pos>} ->
    {B.contains(t, c) == True{} : Bool} -> Witness(S.Ctx{w, h, n, rows, its}, c),
  ihn: @l: T.Grid(Bool) -> {S.loop(t, l <> found, todo, part, S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Pos>} ->
    {all_valid(S.Ctx{w, h, n, rows, its}, l <> found) == True{} : Bool} -> {B.contains(t, c) == True{} : Bool} ->
    Witness(S.Ctx{w, h, n, rows, its}, c)) ->
  Witness(S.Ctx{w, h, n, rows, its}, c):
  match b:
    case True{}:
      +ctx = {S.Ctx{w, h, n, rows, its} : S.Ctx}
      loop_none.pick2(ctx, c0, t, c, found, mr, be, val, mt => ihf(e, mt))
    case False{}:
      +ctx = {S.Ctx{w, h, n, rows, its} : S.Ctx}
      loop_none.found(c0, t, found, todo, part, w, h, n, rows, its, val, shP, on0, c, mr,
        loop_found_none(S.search(c0, todo, part, ctx), c0, l => S.loop(t, l <> found, todo, part, ctx), e), ihn)

Uses (25):
  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=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Or
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=contains
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=on_board
  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=shaped
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=Witness
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=all_valid
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=loop_found_none
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=loop_none.found
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=loop_none.pick2
  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=Plan
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=covered
  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
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Seen