2514def sm86EncodeProgramRepeated =
2515 (lambda unrestricted segment : (family SM86Program) .
2516 (lambda unrestricted count : Nat .
2517 (nat-eliminate
2518 (lambda unrestricted nonzero : Nat . (family SM86ProgramEncodingResult))
2519 (constructor
2520 SM86ProgramEncodingResult
2521 SM86ProgramEncodingSucceeded
2522 b""
2523 sm86ProgramTelemetryZero)
2524 (lambda unrestricted predecessor : Nat .
2525 (lambda unrestricted induction : (family SM86ProgramEncodingResult) .
2526 (eliminate
2527 SM86ProgramEncodingResult
2528 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
2529 (family SM86ProgramEncodingResult))
2530 (sm86EncodeProgram segment)
2531 (branch
2532 SM86ProgramEncodingSucceeded
2533 segmentBytes
2534 segmentTelemetry
2535 .
2536 (constructor
2537 SM86ProgramEncodingResult
2538 SM86ProgramEncodingSucceeded
2539 (bytes-builder-build (sm86RepeatedProgramBytesBuilder segmentBytes count))
2540 (sm86ScaleProgramTelemetry segmentTelemetry count)))
2541 (branch
2542 SM86ProgramEncodingFailed
2543 failureIndex
2544 failure
2545 failureTelemetry
2546 .
2547 (constructor
2548 SM86ProgramEncodingResult
2549 SM86ProgramEncodingFailed
2550 failureIndex
2551 failure
2552 failureTelemetry)))))
2553 (naturalNonzero count))))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.