def tensor_source
bendtorch-core@0.1.0.0 · src/tensor/reduction_PROOF.bend:450
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
450def tensor_source(-shape: Shape.Shape, +fuel: Nat, tensor: Core.Tensor<shape>, words: Words<fuel, shape, tensor>) ->
451 Fact<Laws.SourceSum<fuel, shape, tensor, 0n, 0.0, Reduction.tensor_sum(shape, fuel, tensor)>>:
452 Words{values, logical} = words
453 Fact{Laws.SourceSum{unit => meaning_from(shape, fuel, tensor, values, logical, Reduction.tensor_sum(shape, fuel, tensor),
454 {\{Fact: p => p} : Fact<({Laws.loop_value(shape, Reduction.tensor_sum(shape, fuel, tensor)) == Some{Reduction.sequential_sum(values, 0.0)} : Maybe<&2, F32>})> ->
455 {Laws.loop_value(shape, Reduction.tensor_sum(shape, fuel, tensor)) == Some{Reduction.sequential_sum(values, 0.0)} : Maybe<&2, F32>}}(
456 tensor_value(shape, fuel, tensor, values, logical)))}}