2335def sm86EncodeProgramRepeated =
2336 (lambda unrestricted segment : (family SM86Program) .
2337 (lambda unrestricted count : Nat .
2338 (nat-eliminate
2339 (lambda unrestricted nonzero : Nat . (family SM86ProgramEncodingResult))
2340 (constructor
2341 SM86ProgramEncodingResult
2342 SM86ProgramEncodingSucceeded
2343 b""
2344 sm86ProgramTelemetryZero)
2345 (lambda unrestricted predecessor : Nat .
2346 (lambda unrestricted induction : (family SM86ProgramEncodingResult) .
2347 (eliminate
2348 SM86ProgramEncodingResult
2349 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
2350 (family SM86ProgramEncodingResult))
2351 (sm86EncodeProgram segment)
2352 (branch
2353 SM86ProgramEncodingSucceeded
2354 segmentBytes
2355 segmentTelemetry
2356 .
2357 (constructor
2358 SM86ProgramEncodingResult
2359 SM86ProgramEncodingSucceeded
2360 (bytes-builder-build (sm86RepeatedProgramBytesBuilder segmentBytes count))
2361 (sm86ScaleProgramTelemetry segmentTelemetry count)))
2362 (branch
2363 SM86ProgramEncodingFailed
2364 failureIndex
2365 failure
2366 failureTelemetry
2367 .
2368 (constructor
2369 SM86ProgramEncodingResult
2370 SM86ProgramEncodingFailed
2371 failureIndex
2372 failure
2373 failureTelemetry)))))
2374 (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.