TensorBackwardPROOF.spared: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/tensor_backward_PROOF.bend as TensorBackwardPROOF
Lines 126-131 of bendtorch-core@0.1.0.0/src/autograd/tensor_backward_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward_PROOF.bend&start_line=126&end_line=131

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend as Backward
import bendtorch-core@0.1.0.0/src/autograd/tensor_backward_LAWS.bend as Laws

def spared(+id: Nat, items: List<&1, Backward.Contribution>) -> {Laws.reaches(id, Backward.kept_others(id, items)) == False{} : Bool}:
  match items:
    case Nil{}:
      {==}
    case Con{Backward.Contribution{+target, +shape, gradient}, rest}:
      spared_one(id, target, shape, gradient, rest, spared(id, rest), Shape.bool_case(Nat.is_eq(id, target)))

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/tensor_backward.bend&name=Contribution
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=kept_others
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward_LAWS.bend&name=reaches
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward_PROOF.bend&name=spared_one
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=bool_case