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

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/tensor/word_conversion.bend as Conversion

# The words of the tensor in index order, as the law of `natural_sum_loop`
# names them.
def tensor_words(+shape: Shape.Shape, tensor: Core.Tensor<shape>) -> Fact<Words<Shape.elements(shape), shape, tensor>>:
  Fact{{\{Fact: p => p} : Fact<(Words<Shape.elements(shape), shape, tensor>)> -> Words<Shape.elements(shape), shape, tensor>}(words_of(Shape.elements(shape), shape, tensor, Reduction.natural_sum_loop(Shape.elements(shape), shape, tensor, 0n, 0.0),
    {\{Laws.SourceSum: meaning => meaning(Unit{})} :
      Laws.SourceSum<Shape.elements(shape), shape, tensor, 0n, 0.0, Reduction.natural_sum_loop(Shape.elements(shape), shape, tensor, 0n, 0.0)> ->
      Laws.LoopMeaning(Shape.elements(shape), shape, tensor, 0n, 0.0, Reduction.natural_sum_loop(Shape.elements(shape), shape, tensor, 0n, 0.0))}(
      Laws.successful_loop_interpretation(Shape.elements(shape), shape, tensor, 0n, 0.0)),
    sum_loop_status(Shape.elements(shape), shape, tensor, 0n, 0.0,
      %Equal.sym(Nat, Nat.add(Shape.elements(shape), 0n), Shape.elements(shape), add_zero(Shape.elements(shape))) : Shape.LE(_, Shape.elements(shape))
      Shape.LE.from(Shape.elements(shape), Shape.elements(shape), Equal.sym(Bool, Nat.is_le(Shape.elements(shape), Shape.elements(shape)), True{}, Conversion.le_reflexive(Shape.elements(shape)))))))}

Uses (21):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=LE
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=LE.from
  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/shape/core.bend&name=elements
  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=natural_sum_loop
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend&name=LoopMeaning
  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=successful_loop_interpretation
  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=add_zero
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&name=sum_loop_status
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&name=words_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=le_reflexive