ReductionPROOF.tensor_value: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend as ReductionPROOF
Lines 407-420 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=407&end_line=420

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
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage

# The array fold of `Reduction.sum` adds the tensor's words in index order
# from +0.0.
def tensor_value(-shape: Shape.Shape, +fuel: Nat, tensor: Core.Tensor<shape>, +values: List<&2, F32>,
  logical: Laws.LogicalValues(fuel, shape, tensor, 0n, values)) ->
  Fact<{Laws.loop_value(shape, Reduction.tensor_sum(shape, fuel, tensor)) == Some{Reduction.sequential_sum(values, 0.0)} : Maybe<&2, F32>}>:
  Core.TTensor{storage, exact} = tensor
  match storage:
    case Storage.Empty{}:
      Fact{Equal.cong(F32, Maybe<&2, F32>, x => Some{x}, 0.0, Reduction.sequential_sum(values, 0.0),
        {\{Fact: p => p} : Fact<({0.0 == Reduction.sequential_sum(values, 0.0) : F32})> -> {0.0 == Reduction.sequential_sum(values, 0.0) : F32}}(
          empty_values(shape, exact, fuel, 0n, values, logical)))}
    case Storage.Owned{+depth, +length, array, balanced, valid}:
      owned_value(shape, depth, length, array, balanced, valid, exact, fuel, values, logical, Reduction.array_sum(fuel, 0n, 0.0, array),
        Reduction.array_sum_keeps(depth, array, balanced, fuel, 0n, 0.0, array, {==}), {==})

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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/storage/main.bend&name=Storage
  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=array_sum
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction.bend&name=array_sum_keeps
  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=LogicalValues
  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=empty_values
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&name=owned_value