AlphaGitHub
Source/Packages

Checkpoint.RegionManifest

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

486 lines57 declarations18.9 KiBSHA-256 d7bb0151af81
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 377–388

checkpointManifestValid

Full file
377def checkpointManifestValid =
378  (lambda unrestricted version : Nat .
379    (lambda unrestricted regions : (family StdList (family CheckpointLogicalRegion)) .
380      (lambda unrestricted capture : (family CheckpointCapture) .
381        (lambda unrestricted groups : (family StdList (family CheckpointCapturedRegion)) .
382          (naturalAnd
383            (naturalEqual version checkpointManifestVersion)
384            (naturalAnd
385              (checkpointLogicalRegionsValid regions)
386              (naturalAnd
387                (checkpointCaptureValid capture)
388                (checkpointManifestFrom capture regions 0 groups))))))))

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.