def spared

bendtorch-core@0.1.0.0 · src/autograd/tensor_backward_PROOF.bend:126

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

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