AlphaGitHub
Source/Packages

Checkpoint.NativeRegions

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

901 lines47 declarations40.2 KiBSHA-256 9e8fb104ae0c
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 136–149

nativeRegionEnd

Full file
136def nativeRegionEnd =
137  (lambda unrestricted value : (family NativeRegionCheckpoint) .
138    (eliminate
139      NativeRegionCheckpoint
140      (lambda unrestricted current : (family NativeRegionCheckpoint) . Nat)
141      value
142      (branch
143        NativeRegionCheckpointOf
144        nativeRegionManifest
145        nativeRegionShards
146        nativeRegionEpoch
147        nativeRegionEnd
148        .
149        nativeRegionEnd)))

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.