BackwardPROOF.find_unknown: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend as BackwardPROOF
Lines 307-315 of bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend&start_line=307&end_line=315

import Base
import bendtorch-core@0.1.0.0/src/autograd/backward.bend as Backward

def find_unknown(-A: Data, +xs: List<&2, A>, +id: Nat, +outside: {Nat.is_lt(id, List.length(&2, A, xs)) == False{} : Bool}) ->
  {Backward.find(A, xs, List.length(&2, A, xs), id) == None{} : Maybe<&2, A>}:
  match xs:
    case Nil{}:
      {==}
    case Con{head, tail}:
      %not_lt_succ_ne(id, List.length(&2, A, tail), outside) :
        {Backward.picked(A, head, unit => Backward.find(A, tail, List.length(&2, A, tail), id), _) == None{} : Maybe<&2, A>}
      find_unknown(A, tail, id, not_lt_succ_lt(id, List.length(&2, A, tail), outside))

Uses (10):
  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=List.length
  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=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=find
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=picked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend&name=not_lt_succ_lt
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend&name=not_lt_succ_ne