ProofSolver.order_split.cell: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_solver.bend as ProofSolver
Lines 1978-1988 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=1978&end_line=1988

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 order_split.cell(+c: T.Pos, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +q: T.Pos,
  r: Or({B.same(c, q) == True{} : Bool}, {tcontains(rest, q) == True{} : Bool}),
  ih: {tcontains(rest, q) == True{} : Bool} ->
    {Bool.or(tcontains(S.nears(rest), q), tcontains(S.fars(rest), q)) == True{} : Bool}) ->
  {Bool.or(tcontains(S.nears(S.Todo{c, rel} <> rest), q), tcontains(S.fars(S.Todo{c, rel} <> rest), q)) == True{} : Bool}:
  match r:
    case Inl{cq}:
      order_split.self(c, rel, rest, q, cq, S.has_rel(S.Todo{c, rel}), {==})
    case Inr{m}:
      order_split.rest(S.Todo{c, rel}, rest, q, S.has_rel(S.Todo{c, rel}),
        or_cases(tcontains(S.nears(rest), q), tcontains(S.fars(rest), q), ih(m)))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  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=minebender-game@1.0.0.0/board.bend&name=same
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=or_cases
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=order_split.rest
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=order_split.self
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=tcontains
  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=fars
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=has_rel
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=nears
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos