def write_owner
bendtorch-core@0.1.0.0 · src/autograd/gradient_PROOF.bend:163
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
163def write_owner(-shape: Shape.Shape, -contribution: Core.Dynamic, pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>) ->
164 Holds<{step_owner(shape, Gradient.step_write(shape, contribution, pair)) == contribution : Core.Dynamic}>:
165 (total, result) = pair
166 match result:
167 case Fail{error}:
168 Holds{{==}}
169 case Done{unit}:
170 Holds{{==}}