def Values
bendtorch-core@0.1.0.0 · src/autograd/gradient_PROOF.bend:235
import bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend as GradientPROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/autograd/gradient.bend as Gradient
import bendtorch-core@0.1.0.0/src/autograd/gradient_LAWS.bend as Laws
235def Values(+shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +limit: Nat, after: Gradient.Slot) -> Type:
236 @+index: U32 -> @inside: Laws.Inside(shape, index) ->
237 {Laws.held_observe(after, index) ==
238 partial(Nat.is_lt(U32.to_nat(index), limit), Core.checked_observe(shape, original, index), Core.checked_observe_dynamic(contribution, index)) : Maybe<&2, F32>}