736def checkpointWord64Decimal =
737 (lambda unrestricted value : (family ModelWord64) .
738 (nat-eliminate
739 (lambda unrestricted isZero : Nat . (family CheckpointBytesResult))
740 (checkpointDecimalWithFuel (byte-to-nat (byte 20)) (checkpointWord64ToNatural value))
741 (lambda unrestricted predecessor : Nat .
742 (lambda unrestricted induction : (family CheckpointBytesResult) .
743 (constructor CheckpointBytesResult CheckpointBytesSucceeded b"0")))
744 (modelWord64IsZero value)))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.