Signed.times: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/signed.bend as Signed
Lines 141-154 of bendtorch-core@0.1.0.0/src/tensor/signed.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed.bend&start_line=141&end_line=154

import Base

# A nonzero size times the product of the sizes after it. A size past the
# bound makes any nonzero product pass it, so it is never multiplied.
def times(+bound: Nat, size: Nat, rest: Product) -> Product:
  match size:
    case 0n:
      ZeroProduct{}
    case 1n+(+less):
      match rest:
        case ZeroProduct{}:
          ZeroProduct{}
        case Within{+product}:
          scaled(bound, 1n+less, product, Nat.is_lt(bound, 1n+less))
        case Beyond{}:
          Beyond{}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed.bend&name=Product
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/signed.bend&name=scaled