ReductionPROOF.tensor_source: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend as ReductionPROOF
Lines 450-456 of bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&start_line=450&end_line=456

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

def tensor_source(-shape: Shape.Shape, +fuel: Nat, tensor: Core.Tensor<shape>, words: Words<fuel, shape, tensor>) ->
  Fact<Laws.SourceSum<fuel, shape, tensor, 0n, 0.0, Reduction.tensor_sum(shape, fuel, tensor)>>:
  Words{values, logical} = words
  Fact{Laws.SourceSum{unit => meaning_from(shape, fuel, tensor, values, logical, Reduction.tensor_sum(shape, fuel, tensor),
    {\{Fact: p => p} : Fact<({Laws.loop_value(shape, Reduction.tensor_sum(shape, fuel, tensor)) == Some{Reduction.sequential_sum(values, 0.0)} : Maybe<&2, F32>})> ->
      {Laws.loop_value(shape, Reduction.tensor_sum(shape, fuel, tensor)) == Some{Reduction.sequential_sum(values, 0.0)} : Maybe<&2, F32>}}(
      tensor_value(shape, fuel, tensor, values, logical)))}}

Uses (13):
  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=Nat
  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/tensor/core.bend&name=Tensor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction.bend&name=sequential_sum
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction.bend&name=tensor_sum
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend&name=SourceSum
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend&name=loop_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&name=Fact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&name=Words
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&name=meaning_from
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&name=tensor_value