def zero_inv

bendtorch-core@0.1.0.0 · src/autograd/reduce_PROOF.bend:129

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/tensor/construction_contract_PROOF.bend as ConstructionProof
import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Observation

129def zero_inv(+plan: Shape.BroadcastPlan, +values: List<&2, F32>, +target: Shape.Shape, output: Core.Tensor<target>,
130  -same: {Done{output} == Core.new(target, 0.0) : Result<&2, &1, Core.Error, Core.Tensor<target>>}) ->
131  Holds<Inv(plan, values, target, 0n, output)>:
132  Holds{index => inside => Equal.trans(Maybe<&2, F32>, Core.checked_observe(target, output, index),
133    Core.read_value(target, Core.read_flat(target, output, index)), Some{0.0},
134    Equal.sym(Maybe<&2, F32>, Core.read_value(target, Core.read_flat(target, output, index)), Core.checked_observe(target, output, index),
135      {\{Core.SourceRead: meaning => meaning} : Core.SourceRead<target, output, index> ->
136        {Core.read_value(target, Core.read_flat(target, output, index)) == Core.checked_observe(target, output, index) : Maybe<&2, F32>}}(
137        Core.source_read_model(target, output, index))),
138    %Equal.sym(Result<&2, &1, Core.Error, Core.Tensor<target>>, Done{output}, Core.new(target, 0.0), same) :
139      {Observation.point(target, index, _) == Some{0.0} : Maybe<&2, F32>}
140    ConstructionProof.point_value(target, 0.0, index, inside))}