516def nativeTelemetryFillSources =
517 (lambda unrestricted applicationBytes : Nat .
518 (lambda unrestricted ordinaryCapacity : Nat .
519 (lambda unrestricted reservedCapacity : Nat .
520 (lambda unrestricted recipe : (family TelemetryRecordPlan) .
521 (lambda unrestricted values : (family NativeTelemetrySourceValues) .
522 (lambda unrestricted iterationAt : Nat .
523 (lambda unrestricted identity : Bytes .
524 (lambda unrestricted tail : (family NativePhysicalCommands) .
525 (eliminate
526 TelemetryRecordPlan
527 (lambda unrestricted current : (family TelemetryRecordPlan) .
528 (family NativePhysicalCommands))
529 recipe
530 (branch
531 TelemetryRecordReady
532 parts
533 template
534 .
535 (app
536 (nat-eliminate
537 (lambda unrestricted count : Nat .
538 (pi unrestricted commands : (family NativePhysicalCommands) .
539 (family NativePhysicalCommands)))
540 (lambda unrestricted commands : (family NativePhysicalCommands) .
541 commands)
542 (lambda unrestricted index : Nat .
543 (lambda unrestricted induction : (pi unrestricted commands : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
544 (lambda unrestricted commands : (family NativePhysicalCommands) .
545 (nativeTelemetryEmitSource
546 (nativeTelemetryPolicyState
547 (naturalAdd
548 (captureValuesScratchAt
549 applicationBytes
550 ordinaryCapacity
551 reservedCapacity)
552 (naturalMultiply index captureWordBytes)))
553 (aosChoose
554 (family NativePhysicalOperand)
555 (telemetryRecordWordRequired parts index)
556 (nativeTelemetrySourceOperand
557 (nativeTelemetrySourceAt values index))
558 (nativeLaunchRecipeImmediate 0))
559 iterationAt
560 identity
561 (induction commands)))))
562 captureValueWords)
563 tail))
564 (branch
565 TelemetryRecordRefused
566 reason
567 .
568 (nativeLaunchRecipeCommand
569 (constructor
570 NativePhysicalOperation
571 NativePhysicalMachineRoutine
572 b""
573 (nativeLaunchRecipeArguments
574 (nativeLaunchRecipeImmediate 0)
575 (nativeLaunchRecipeImmediate 0)
576 (nativeLaunchRecipeImmediate 0)
577 (nativeLaunchRecipeImmediate 0))
578 (constructor NativePhysicalResultBinding NativePhysicalDiscardResult))
579 identity
580 tail)))))))))))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.