def word_below
bendtorch-core@0.1.0.0 · src/tensor/permute_build_proof.bend:339
import bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend as PermuteBuildProof
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
339def word_below(+shape: Shape.Shape, +other: Nat, +earlier: {Nat.is_lt(other, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
340 {U32.to_nat(U32.from_nat(other)) == other : Nat}:
341 Conversion.natural_word_exact(other, Shape.count(shape),
342 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.logical_numel(Shape.dimensions(shape)),
343 Equal.trans(Nat, U32.to_nat(Shape.count(shape)), Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)),
344 Conversion.shape_count_exact(shape), Shape.elements_exact(shape))) : {Nat.is_le(other, _) == True{} : Bool}
345 Conversion.lt_le(other, Shape.logical_numel(Shape.dimensions(shape)), earlier))