AlphaGitHub
Source/Packages

Runtime.TelemetryPublication

packages/execution/src/Runtime/TelemetryPublication.alpha

627 lines66 declarations23.6 KiBSHA-256 12de32412e73
Download exact fileView at revision426597bda5753d86c4

def · lines 257–264

publicationWholeArenaBytesForBody

Full file
257def publicationWholeArenaBytesForBody =
258  (lambda unrestricted applicationBytes : Nat .
259    (lambda unrestricted ordinaryCapacity : Nat .
260      (lambda unrestricted reservedCapacity : Nat .
261        (lambda unrestricted bodyBytes : Nat .
262          (naturalAdd
263            (publicationBase applicationBytes ordinaryCapacity reservedCapacity)
264            (publicationArenaBytesForBody bodyBytes))))))

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.