def initial_inv
bendtorch-core@0.1.0.0 · src/autograd/gradient_PROOF.bend:497
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
497def initial_inv(+shape: Shape.Shape, total: Core.Tensor<shape>, -contribution: Core.Dynamic) ->
498 Holds<Inv(shape, total, contribution, 0n, total)>:
499 Holds{index => inside =>
500 %Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), 0n), False{}, below_zero(U32.to_nat(index))) :
501 {Core.checked_observe(shape, total, index) ==
502 partial(_, Core.checked_observe(shape, total, index), Core.checked_observe_dynamic(contribution, index)) : Maybe<&2, F32>}
503 {==}}