def empty_below
bendtorch-core@0.1.0.0 · src/tensor/permute_build_proof.bend:485
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/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
485def empty_below(-shape: Shape.Shape, +other: Nat, exact: {Lifecycle.logical_length(Storage.Empty{}) == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
486 earlier: {Nat.is_lt(other, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> Empty:
487 Arith.lt_zero(other,
488 %Equal.sym(Nat, Lifecycle.logical_length(Storage.Empty{}), Shape.logical_numel(Shape.dimensions(shape)), exact) : {Nat.is_lt(other, _) == True{} : Bool}
489 earlier)