449def magnitudeDouble =
450 (lambda unrestricted digits : Bytes .
451 (bytes-builder-build
452 (app
453 (bytes-eliminate
454 (lambda unrestricted rest : Bytes . (pi unrestricted carry : Nat . BytesBuilder))
455 (lambda unrestricted carry : Nat .
456 (app
457 (nat-eliminate
458 (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . BytesBuilder))
459 (lambda unrestricted force : Nat . (bytes-builder-empty))
460 (lambda unrestricted predecessor : Nat .
461 (lambda unrestricted induction : (pi unrestricted force : Nat . BytesBuilder) .
462 (lambda unrestricted force : Nat .
463 (bytes-builder-chunk (bytes-cons (byte 1) b"")))))
464 carry)
465 zero))
466 (lambda unrestricted head : Byte .
467 (lambda unrestricted tail : Bytes .
468 (lambda unrestricted continue : (pi unrestricted carry : Nat . BytesBuilder) .
469 (lambda unrestricted carry : Nat .
470 (app
471 (nat-eliminate
472 (lambda unrestricted flag : Nat .
473 (pi unrestricted force : Nat . BytesBuilder))
474 (lambda unrestricted force : Nat .
475 (app
476 (lambda unrestricted reduced : Nat .
477 (bytes-builder-append
478 (bytes-builder-chunk
479 (bytes-cons
480 (nat-to-byte
481 (Std.Natural/naturalAdd
482 carry
483 (Std.Natural/naturalAdd reduced reduced)))
484 b""))
485 (continue (succ zero))))
486 (byte-to-nat
487 (nat-to-byte
488 (Std.Natural/naturalAdd (byte-to-nat head) (byte-to-nat (byte 251)))))))
489 (lambda unrestricted predecessor : Nat .
490 (lambda unrestricted induction : (pi unrestricted force : Nat . BytesBuilder) .
491 (lambda unrestricted force : Nat .
492 (bytes-builder-append
493 (bytes-builder-chunk
494 (bytes-cons
495 (nat-to-byte
496 (Std.Natural/naturalAdd
497 carry
498 (Std.Natural/naturalAdd (byte-to-nat head) (byte-to-nat head))))
499 b""))
500 (continue zero)))))
501 (byte-less-than head (byte 5)))
502 zero)))))
503 digits)
504 zero)))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.