AlphaGitHub
Source/Packages

Checkpoint.Schema

packages/execution/persistence/src/Checkpoint/Schema.alpha

2,376 lines254 declarations94.9 KiBSHA-256 c49b7c5718ad
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 588–610

checkpointNaturalWord64

Full file
588def checkpointNaturalWord64 =
589  (lambda unrestricted code : (family CheckpointErrorCode) .
590    (lambda unrestricted value : Nat .
591      (nat-eliminate
592        (lambda unrestricted fits : Nat . (family CheckpointWord64Result))
593        (constructor CheckpointWord64Result CheckpointWord64Failed code)
594        (lambda unrestricted predecessor : Nat .
595          (lambda unrestricted induction : (family CheckpointWord64Result) .
596            (constructor
597              CheckpointWord64Result
598              CheckpointWord64Succeeded
599              (constructor
600                ModelWord64
601                ModelWord64Value
602                (checkpointNaturalByteAt value zero)
603                (checkpointNaturalByteAt value (byte-to-nat (byte 8)))
604                (checkpointNaturalByteAt value (byte-to-nat (byte 16)))
605                (checkpointNaturalByteAt value (byte-to-nat (byte 24)))
606                (checkpointNaturalByteAt value (byte-to-nat (byte 32)))
607                (checkpointNaturalByteAt value (byte-to-nat (byte 40)))
608                (checkpointNaturalByteAt value (byte-to-nat (byte 48)))
609                (checkpointNaturalByteAt value (byte-to-nat (byte 56)))))))
610        (naturalIsZero (naturalDivideUnchecked value (naturalPowerOfTwo (byte-to-nat (byte 64))))))))

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.