AlphaGitHub
Source/Packages

Runtime.TelemetryRecord

packages/execution/src/Runtime/TelemetryRecord.alpha

774 lines93 declarations28.3 KiBSHA-256 d4129743e998
Download exact fileView at revision426597bda5753d86c4

def · lines 512–535

telemetryRecordArenaResidents

Full file
512def telemetryRecordArenaResidents =
513  (lambda unrestricted base : Nat .
514    (lambda unrestricted parts : (family TelemetryRecordParts) .
515      (constructor
516        ArenaResidents
517        ArenaResidentsNext
518        (constructor
519          ArenaResident
520          ArenaResidentValue
521          b"record-status"
522          base
523          telemetryRecordStatusBytes
524          captureWordBytes)
525        (constructor
526          ArenaResidents
527          ArenaResidentsNext
528          (constructor
529            ArenaResident
530            ArenaResidentValue
531            b"record-json"
532            (naturalAdd base telemetryRecordAt)
533            (bytes-length (telemetryRecordPartBytes parts))
534            1)
535          (constructor ArenaResidents ArenaResidentsEnd)))))

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.