def length_below
bendtorch-core@0.1.0.0 · src/tensor/permute_build_proof.bend:347
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
347def length_below(+shape: Shape.Shape, +n: Nat, +exact: {n == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +other: Nat,
348 +earlier: {Nat.is_lt(other, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
349 {Nat.is_lt(U32.to_nat(U32.from_nat(other)), n) == True{} : Bool}:
350 %Equal.sym(Nat, U32.to_nat(U32.from_nat(other)), other, word_below(shape, other, earlier)) : {Nat.is_lt(_, n) == True{} : Bool}
351 %Equal.sym(Nat, n, Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(other, _) == True{} : Bool}
352 earlier