def lt_count

bendtorch-core@0.1.0.0 · src/tensor/contracts/pointwise_proof.bend:150

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/read_contract.bend as Reads

150def lt_count(+number: Nat, +shape: Shape.Shape,
151  below: {Nat.is_lt(number, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
152  {Nat.is_lt(number, U32.to_nat(Shape.count(shape))) == True{} : Bool}:
153  %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.logical_numel(Shape.dimensions(shape)), Reads.count_exact(shape)) :
154    {Nat.is_lt(number, _) == True{} : Bool}
155  below