AlphaGitHub
Source/Packages

Runtime.RegionFrame

packages/execution/src/Runtime/RegionFrame.alpha

320 lines27 declarations14.1 KiBSHA-256 31efcb569418
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 310–320

receiveRegionFrame

Full file
310def receiveRegionFrame =
311  (lambda unrestricted identity : (family RegionTransferIdentity) .
312    (lambda unrestricted expectedBytes : Nat .
313      (lambda unrestricted headerBudget : Nat .
314        (lambda unrestricted phase : (family TransferPhase) .
315          (lambda unrestricted frame : Bytes .
316            (regionFrameRequire
317              (naturalEqual (transferPhaseCode phase) 2)
318              (constructor RegionFrameFailure RegionFrameWrongPhase)
319              (lambda unrestricted delayed : Nat .
320                (decodeRegionFrame identity expectedBytes headerBudget frame))))))))

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.