527def nativeTelemetrySinkBegin =
528 (lambda unrestricted path : Bytes .
529 (lambda unrestricted record : (family NativeTelemetryEncodedRecord) .
530 (eliminate
531 NativeTelemetryEncodedRecord
532 (lambda unrestricted current : (family NativeTelemetryEncodedRecord) .
533 (family NativeTelemetrySinkDecision))
534 record
535 (branch
536 NativeTelemetryEncodedRecordValue
537 bytes
538 extent
539 digest
540 identity
541 .
542 (app
543 (lambda unrestricted initialState : (family NativeTelemetrySinkState) .
544 (nat-eliminate
545 (lambda unrestricted current : Nat . (family NativeTelemetrySinkDecision))
546 (constructor
547 NativeTelemetrySinkDecision
548 NativeTelemetrySinkRejected
549 (constructor NativeTelemetryErrorCode NativeTelemetryPathEmpty)
550 initialState)
551 (lambda unrestricted pathPredecessor : Nat .
552 (lambda unrestricted ignoredPath : (family NativeTelemetrySinkDecision) .
553 (nat-eliminate
554 (lambda unrestricted current : Nat . (family NativeTelemetrySinkDecision))
555 (constructor
556 NativeTelemetrySinkDecision
557 NativeTelemetrySinkRejected
558 (constructor NativeTelemetryErrorCode NativeTelemetryRecordEmpty)
559 initialState)
560 (lambda unrestricted recordPredecessor : Nat .
561 (lambda unrestricted ignoredRecord : (family NativeTelemetrySinkDecision) .
562 (constructor
563 NativeTelemetrySinkDecision
564 NativeTelemetrySinkContinue
565 initialState
566 (constructor
567 NativeTelemetrySinkAction
568 NativeTelemetrySinkIssueSyscall
569 (nativeTelemetryOpenAppendRequest path)))))
570 (bytes-length bytes))))
571 (bytes-length path)))
572 (constructor
573 NativeTelemetrySinkState
574 NativeTelemetrySinkStateValue
575 path
576 record
577 (constructor NativeTelemetrySinkPhase NativeTelemetrySinkOpening)
578 (constructor NativeTelemetryOptionalDescriptor NativeTelemetryNoDescriptor)
579 (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.