AlphaGitHub
Source/Packages

Runtime.TelemetryValue

packages/execution/src/Runtime/TelemetryValue.alpha

138 lines12 declarations5.1 KiBSHA-256 009e6a09feb8
Download exact fileView at revision426597bda5753d86c4

def · lines 112–124

telemetryWordCellAdmission

Full file
112def telemetryWordCellAdmission =
113  (lambda unrestricted offset : Nat .
114    (lambda unrestricted sourceExtent : Nat .
115      (lambda unrestricted destinationExtent : Nat .
116        (aosChoose
117          Nat
118          (naturalAnd
119            (telemetryRangeFits offset captureWordBytes captureRecordBytes)
120            (naturalAnd
121              (telemetryRangeFits offset captureWordBytes sourceExtent)
122              (naturalLessOrEqual telemetryDecimalCellBytes destinationExtent)))
123          0
124          4))))

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.