535def magnitudeMultiply =
536 (lambda unrestricted left : Bytes .
537 (lambda unrestricted right : Bytes .
538 (bytes-eliminate
539 (lambda unrestricted rest : Bytes . Bytes)
540 b""
541 (lambda unrestricted head : Byte .
542 (lambda unrestricted tail : Bytes .
543 (lambda unrestricted continue : Bytes .
544 (magnitudeAdd
545 (magnitudeMultiplyDigit left head)
546 (app
547 (nat-eliminate
548 (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . Bytes))
549 (lambda unrestricted force : Nat . (bytes-cons (byte 0) continue))
550 (lambda unrestricted predecessor : Nat .
551 (lambda unrestricted induction : (pi unrestricted force : Nat . Bytes) .
552 (lambda unrestricted force : Nat . b"")))
553 (bytes-equal continue b""))
554 zero)))))
555 right)))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.