AlphaGitHub
Source/Packages

Runtime.TelemetryCapture

packages/execution/src/Runtime/TelemetryCapture.alpha

246 lines33 declarations8.5 KiBSHA-256 79eb60f3fee4
Download exact fileView at revision426597bda5753d86c4

def · lines 202–214

captureArenaCertificate

Full file
202def captureArenaCertificate =
203  (lambda unrestricted applicationBytes : Nat .
204    (lambda unrestricted ordinaryCapacity : Nat .
205      (lambda unrestricted reservedCapacity : Nat .
206        (naturalAnd
207          (naturalLessOrEqual
208            (captureArenaBytes applicationBytes ordinaryCapacity reservedCapacity)
209            captureExtentMaximum)
210          (naturalAnd
211            (naturalLessOrEqual 2 reservedCapacity)
212            (arenaCertificate
213              (captureArenaBytes applicationBytes ordinaryCapacity reservedCapacity)
214              (captureArenaResidents applicationBytes ordinaryCapacity reservedCapacity)))))))

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.