def sum_source_result
bendtorch-core@0.1.0.0 · src/tensor/reduction_PROOF.bend:615
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
615def sum_source_result(+shape: Shape.Shape, -original: Core.Tensor<shape>,
616 result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>,
617 -source: Laws.SourceSum<Shape.logical_numel(Shape.dimensions(shape)), shape, original, 0n, 0.0, result>,
618 -preservation: Laws.Preserved<shape, original, result>) -> Laws.SourceSumResult<shape, original, Reduction.sum_result(shape, result)>:
619 match result:
620 case Fail{error}:
621 Laws.SourceSumResult{unit => Unit{}}
622 case Done{pair}:
623 (retained, +value) = pair
624 Laws.SourceSumResult{unit =>
625 prove : @certificates: Laws.SourceSum<Shape.logical_numel(Shape.dimensions(shape)), shape, original, 0n, 0.0,
626 (Done{(retained, value)} : Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>)> &
627 Laws.Preserved<shape, original, (Done{(retained, value)} : Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>)> ->
628 Laws.SumResultMeaning(shape, original, Reduction.sum_result(shape, Done{(retained, value)})) =
629 \{Tuple: \{Laws.SourceSum: meaning => \{Laws.Preserved: kept =>
630 build : @meaning: Laws.SumMeaning<Shape.logical_numel(Shape.dimensions(shape)), shape, original, 0n, 0.0, value> ->
631 Laws.SumResultMeaning(shape, original, Reduction.sum_result(shape, Done{(retained, value)})) =
632 \{Laws.SumMeaning: values => logical => fold =>
633 Laws.SumResult{values, logical,
634 Equal.cong(F32, Maybe<&2, F32>, x => Some{x}, value, Reduction.sequential_sum(values, 0.0), fold), kept}}
635 build(meaning(Unit{}))}}}
636 prove((source, preservation))}