685def checkpointDecimalWithFuel =
686 (lambda unrestricted fuel : Nat .
687 (nat-eliminate
688 (lambda unrestricted current : Nat .
689 (pi unrestricted value : Nat . (family CheckpointBytesResult)))
690 (lambda unrestricted value : Nat .
691 (nat-eliminate
692 (lambda unrestricted isZero : Nat . (family CheckpointBytesResult))
693 (constructor
694 CheckpointBytesResult
695 CheckpointBytesFailed
696 (constructor CheckpointErrorCode CheckpointCanonicalNumberOverflow))
697 (lambda unrestricted predecessor : Nat .
698 (lambda unrestricted induction : (family CheckpointBytesResult) .
699 (constructor CheckpointBytesResult CheckpointBytesSucceeded b"")))
700 (naturalIsZero value)))
701 (lambda unrestricted predecessor : Nat .
702 (lambda unrestricted induction : (pi unrestricted value : Nat . (family CheckpointBytesResult)) .
703 (lambda unrestricted value : Nat .
704 (nat-eliminate
705 (lambda unrestricted isZero : Nat . (family CheckpointBytesResult))
706 (eliminate
707 CheckpointBytesResult
708 (lambda unrestricted current : (family CheckpointBytesResult) .
709 (family CheckpointBytesResult))
710 (induction (naturalDivideUnchecked value (byte-to-nat (byte 10))))
711 (branch
712 CheckpointBytesSucceeded
713 prefix
714 .
715 (constructor
716 CheckpointBytesResult
717 CheckpointBytesSucceeded
718 (bytes-append
719 prefix
720 (bytes
721 (nat-to-byte
722 (naturalAdd
723 (byte-to-nat (byte 48))
724 (naturalModuloUnchecked value (byte-to-nat (byte 10)))))))))
725 (branch
726 CheckpointBytesFailed
727 code
728 .
729 (constructor CheckpointBytesResult CheckpointBytesFailed code)))
730 (lambda unrestricted zeroPredecessor : Nat .
731 (lambda unrestricted zeroInduction : (family CheckpointBytesResult) .
732 (constructor CheckpointBytesResult CheckpointBytesSucceeded b"")))
733 (naturalIsZero value)))))
734 fuel))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.