def tensor_words

bendtorch-core@0.1.0.0 · src/tensor/reduction_PROOF.bend:638

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

638# The words of the tensor in index order, as the law of `natural_sum_loop`
639# names them.
640def tensor_words(+shape: Shape.Shape, tensor: Core.Tensor<shape>) -> Fact<Words<Shape.elements(shape), shape, tensor>>:
641  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),
642    {\{Laws.SourceSum: meaning => meaning(Unit{})} :
643      Laws.SourceSum<Shape.elements(shape), shape, tensor, 0n, 0.0, Reduction.natural_sum_loop(Shape.elements(shape), shape, tensor, 0n, 0.0)> ->
644      Laws.LoopMeaning(Shape.elements(shape), shape, tensor, 0n, 0.0, Reduction.natural_sum_loop(Shape.elements(shape), shape, tensor, 0n, 0.0))}(
645      Laws.successful_loop_interpretation(Shape.elements(shape), shape, tensor, 0n, 0.0)),
646    sum_loop_status(Shape.elements(shape), shape, tensor, 0n, 0.0,
647      %Equal.sym(Nat, Nat.add(Shape.elements(shape), 0n), Shape.elements(shape), add_zero(Shape.elements(shape))) : Shape.LE(_, Shape.elements(shape))
648      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)))))))}