GradientPROOF.unset_zeros: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend as GradientPROOF
Lines 113-133 of bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&start_line=113&end_line=133

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend as Allocation
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
import bendtorch-core@0.1.0.0/src/autograd/gradient_LAWS.bend as Laws

def unset_zeros(+shape: Shape.Shape, result: Result<&2, &1, Core.Error, Core.Tensor<shape>>,
  -same: {result == Core.new(shape, 0.0) : Result<&2, &1, Core.Error, Core.Tensor<shape>>},
  -done: Allocation.TensorDone<shape, result>) ->
  Laws.ZerosModel<shape, Core.construct_values(shape, result)>:
  match result:
    case Fail{error}:
      Laws.ZerosModel{
        {\{Allocation.TensorDone: tensor => equal => Arith.clash(Equal.cong(Result<&2, &1, Core.Error, Core.Tensor<shape>>, Bool,
          found => Result.is_done(&2, &1, Core.Error, Core.Tensor<shape>, found), Fail{error}, Done{tensor},
          Equal.sym(Result<&2, &1, Core.Error, Core.Tensor<shape>>, Done{tensor}, Fail{error}, equal)))} :
          Allocation.TensorDone<shape, Fail{error}> -> Empty}(done)}
    case Done{tensor}:
      Laws.ZerosModel{({==}, index => inside => Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, tensor, index),
        Core.read_value(shape, Core.read_flat(shape, tensor, index)), Some{0.0},
        Equal.sym(Maybe<&2, F32>, Core.read_value(shape, Core.read_flat(shape, tensor, index)), Core.checked_observe(shape, tensor, index),
          {\{Core.SourceRead: meaning => meaning} : Core.SourceRead<shape, tensor, index> ->
            {Core.read_value(shape, Core.read_flat(shape, tensor, index)) == Core.checked_observe(shape, tensor, index) : Maybe<&2, F32>}}(
            Core.source_read_model(shape, tensor, index))),
        %Equal.sym(Result<&2, &1, Core.Error, Core.Tensor<shape>>, Done{tensor}, Core.new(shape, 0.0), same) :
          {Observation.point(shape, index, _) == Some{0.0} : Maybe<&2, F32>}
        ConstructionProof.point_value(shape, 0.0, index, inside)))}

Uses (25):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result.is_done
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_LAWS.bend&name=ZerosModel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=clash
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/allocation_spec.bend&name=TensorDone
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_contract_PROOF.bend&name=point_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=SourceRead
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=checked_observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=construct_values
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=new
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=read_flat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=read_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=source_read_model
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/observation.bend&name=point