BackwardPROOF.pass_reached: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend as BackwardPROOF
Lines 246-254 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=246&end_line=254

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

def pass_reached(nodes: List<&2, Backward.Node>, +count: Nat, +output: Nat) ->
  {Laws.somes(Backward.pass(nodes, count, output)) == Laws.reached(nodes, count, output) : List<&2, Bool>}:
  match nodes count:
    case Nil{} count:
      {==}
    case Con{node, rest} 0n:
      {==}
    case Con{+node, +rest} 1n+below:
      chosen_reached(node, rest, below, output, Nat.is_eq(below, output), pass_reached(rest, below, output))

Uses (9):
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=Node
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=pass
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=reached
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=somes
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend&name=chosen_reached