600def nativeTelemetrySinkBegin =
601 (lambda unrestricted path : Bytes .
602 (lambda unrestricted record : (family NativeTelemetryEncodedRecord) .
603 (eliminate
604 NativeTelemetryEncodedRecord
605 (lambda unrestricted current : (family NativeTelemetryEncodedRecord) .
606 (family NativeTelemetrySinkDecision))
607 record
608 (branch
609 NativeTelemetryEncodedRecordValue
610 bytes
611 extent
612 digest
613 identity
614 .
615 (app
616 (lambda unrestricted initialState : (family NativeTelemetrySinkState) .
617 (nat-eliminate
618 (lambda unrestricted current : Nat . (family NativeTelemetrySinkDecision))
619 (constructor
620 NativeTelemetrySinkDecision
621 NativeTelemetrySinkRejected
622 (constructor NativeTelemetryErrorCode NativeTelemetryPathEmpty)
623 initialState)
624 (lambda unrestricted pathPredecessor : Nat .
625 (lambda unrestricted ignoredPath : (family NativeTelemetrySinkDecision) .
626 (nat-eliminate
627 (lambda unrestricted current : Nat . (family NativeTelemetrySinkDecision))
628 (constructor
629 NativeTelemetrySinkDecision
630 NativeTelemetrySinkRejected
631 (constructor NativeTelemetryErrorCode NativeTelemetryRecordEmpty)
632 initialState)
633 (lambda unrestricted recordPredecessor : Nat .
634 (lambda unrestricted ignoredRecord : (family NativeTelemetrySinkDecision) .
635 (constructor
636 NativeTelemetrySinkDecision
637 NativeTelemetrySinkContinue
638 initialState
639 (constructor
640 NativeTelemetrySinkAction
641 NativeTelemetrySinkIssueSyscall
642 (nativeTelemetryOpenAppendRequest path)))))
643 (bytes-length bytes))))
644 (bytes-length path)))
645 (constructor
646 NativeTelemetrySinkState
647 NativeTelemetrySinkStateValue
648 path
649 record
650 (constructor NativeTelemetrySinkPhase NativeTelemetrySinkOpening)
651 (constructor NativeTelemetryOptionalDescriptor NativeTelemetryNoDescriptor)
652 (nativeTelemetrySinkTelemetryInitial extent)))))))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.