~/jendhub

def dynamic_sum_result

bendtorch-core@0.1.0.0 · src/tensor/reduction_PROOF.bend:665

import bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend as ReductionPROOF
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/reduction.bend as Reduction
import bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend as Laws

665def dynamic_sum_result(+shape: Shape.Shape, -original: Core.Tensor<shape>,
666  result: Result<&2, &1, Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>>,
667  -source: Laws.SourceSumResult<shape, original, result>) -> Laws.SourceDynamicSum<Core.Packed{shape, original}, Reduction.pack_result(shape, result)>:
668  match result:
669    case Fail{error}:
670      Laws.SourceDynamicSum{unit => Unit{}}
671    case Done{pair}:
672      (owner, scalar) = pair
673      Laws.SourceDynamicSum{unit =>
674        claim : @source: Laws.SourceSumResult<shape, original,
675          (Done{(owner, scalar)} : Result<&2, &1, Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>>)> ->
676          Laws.SumResult<shape, original, owner, scalar> = \{Laws.SourceSumResult: meaning => meaning(Unit{})}
677        Laws.DynamicSumSuccess{shape, original, owner, scalar, {==}, {==}, {==}, claim(source)}}

Uses (14)

Used by (1)