ProofSolver.covered_extract.go: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_solver.bend as ProofSolver
Lines 2190-2198 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=2190&end_line=2198

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 covered_extract.go(+ctx: S.Ctx, +l: T.Grid(Bool), +t: List<&2, T.Grid(Bool)>, +c: T.Pos,
  +vl: {S.check(ctx, l) == True{} : Bool},
  r: Or({B.mine(l, c) == True{} : Bool}, {S.covered(t, c) == True{} : Bool}),
  ih: {S.covered(t, c) == True{} : Bool} -> Witness(ctx, c)) -> Witness(ctx, c):
  match r:
    case Inl{m}:
      (l, (vl, m))
    case Inr{cv}:
      ih(cv)

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Either
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Or
  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/board.bend&name=mine
  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/solver.bend&name=Ctx
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=check
  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/types.bend&name=Grid
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos