2412def sm86EncodeProgramRepeated =
2413 (lambda unrestricted segment : (family SM86Program) .
2414 (lambda unrestricted count : Nat .
2415 (nat-eliminate
2416 (lambda unrestricted nonzero : Nat . (family SM86ProgramEncodingResult))
2417 (constructor
2418 SM86ProgramEncodingResult
2419 SM86ProgramEncodingSucceeded
2420 b""
2421 sm86ProgramTelemetryZero)
2422 (lambda unrestricted predecessor : Nat .
2423 (lambda unrestricted induction : (family SM86ProgramEncodingResult) .
2424 (eliminate
2425 SM86ProgramEncodingResult
2426 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
2427 (family SM86ProgramEncodingResult))
2428 (sm86EncodeProgram segment)
2429 (branch
2430 SM86ProgramEncodingSucceeded
2431 segmentBytes
2432 segmentTelemetry
2433 .
2434 (constructor
2435 SM86ProgramEncodingResult
2436 SM86ProgramEncodingSucceeded
2437 (bytes-builder-build (sm86RepeatedProgramBytesBuilder segmentBytes count))
2438 (sm86ScaleProgramTelemetry segmentTelemetry count)))
2439 (branch
2440 SM86ProgramEncodingFailed
2441 failureIndex
2442 failure
2443 failureTelemetry
2444 .
2445 (constructor
2446 SM86ProgramEncodingResult
2447 SM86ProgramEncodingFailed
2448 failureIndex
2449 failure
2450 failureTelemetry)))))
2451 (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.