def times

bendtorch-core@0.1.0.0 · src/tensor/signed.bend:141

import Base

141# A nonzero size times the product of the sizes after it. A size past the
142# bound makes any nonzero product pass it, so it is never multiplied.
143def times(+bound: Nat, size: Nat, rest: Product) -> Product:
144  match size:
145    case 0n:
146      ZeroProduct{}
147    case 1n+(+less):
148      match rest:
149        case ZeroProduct{}:
150          ZeroProduct{}
151        case Within{+product}:
152          scaled(bound, 1n+less, product, Nat.is_lt(bound, 1n+less))
153        case Beyond{}:
154          Beyond{}