Roles: tagged value/availability slot=0, item chain=1, member chain=2,
invalid structure=3. A valid-looking JSON tail cannot change the declared
Alpha structure (for example, a scalar in place of an item-chain tail).
540def telemetryRecordValueRole =
541 (lambda unrestricted value : (family TelemetryCaptureValue) .
542 (eliminate
543 TelemetryCaptureValue
544 (lambda unrestricted current : (family TelemetryCaptureValue) . Nat)
545 value
546 (branch TelemetryConstant constant . 0)
547 (branch TelemetryUnsigned index . 0)
548 (branch TelemetrySigned index . 0)
549 (branch TelemetryFloat32 index . 0)
550 (branch TelemetryFloat64 index . 0)
551 (branch TelemetryReference kind index . 0)
552 (branch TelemetryBytes index width . 0)
553 (branch TelemetryUnavailable state reason . 0)
554 (branch TelemetryList items induction . (aosChoose Nat (naturalEqual induction 1) 0 3))
555 (branch TelemetryItemsEnd . 1)
556 (branch
557 TelemetryItemsNext
558 head
559 tail
560 headInduction
561 tailInduction
562 .
563 (aosChoose
564 Nat
565 (naturalAnd (naturalEqual headInduction 0) (naturalEqual tailInduction 1))
566 1
567 3))
568 (branch TelemetryMap members induction . (aosChoose Nat (naturalEqual induction 2) 0 3))
569 (branch TelemetryMembersEnd . 2)
570 (branch
571 TelemetryMembersNext
572 key
573 head
574 tail
575 headInduction
576 tailInduction
577 .
578 (aosChoose
579 Nat
580 (naturalAnd (naturalEqual headInduction 0) (naturalEqual tailInduction 2))
581 2
582 3))))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.