def find_unknown

bendtorch-core@0.1.0.0 · src/autograd/backward_PROOF.bend:307

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

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