def shape_count_bound

bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:1190

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats

1190def shape_count_bound(+shape: Shape.Shape) -> {Nat.is_le(Shape.elements(shape), 1048576n) == True{} : Bool}:
1191  match shape:
1192    case Shape.SShape{+dimensions, +size, +exact, rank_bound, capacity_bound}:
1193      %Equal.sym(Nat, size, Shape.logical_numel(dimensions), exact) : {Nat.is_le(_, 1048576n) == True{} : Bool}
1194      Equal.sym(Bool, True{}, Nat.is_le(Shape.logical_numel(dimensions), 1048576n),
1195        Nats.le_true(Shape.logical_numel(dimensions), 1048576n, capacity_bound))