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 516–534

checkpointAddChecked

Full file
516def checkpointAddChecked =
517  (lambda unrestricted code : (family CheckpointErrorCode) .
518    (lambda unrestricted left : (family ModelWord64) .
519      (lambda unrestricted right : (family ModelWord64) .
520        (eliminate
521          ModelWord64CheckedResult
522          (lambda unrestricted current : (family ModelWord64CheckedResult) .
523            (family CheckpointWord64Result))
524          (modelWord64AddChecked left right)
525          (branch
526            ModelWord64CheckedSucceeded
527            value
528            .
529            (constructor CheckpointWord64Result CheckpointWord64Succeeded value))
530          (branch
531            ModelWord64CheckedFailed
532            error
533            .
534            (constructor CheckpointWord64Result CheckpointWord64Failed code))))))

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.