3327def decodeDoNamedTail =
3328 (lambda unrestricted quantity : Nat .
3329 (lambda unrestricted binder : Bytes .
3330 (lambda unrestricted arguments : (family TermList) .
3331 (eliminate
3332 TermList
3333 (lambda unrestricted value : (family TermList) . (family DoStepDecodeResult))
3334 arguments
3335 (branch TermListEnd . (constructor DoStepDecodeResult DoStepDecodeFailed))
3336 (branch
3337 TermListNext
3338 arrowTerm
3339 afterArrow
3340 ih_afterArrow
3341 .
3342 (eliminate
3343 TermSpellingResult
3344 (lambda unrestricted result : (family TermSpellingResult) .
3345 (family DoStepDecodeResult))
3346 (termSpelling arrowTerm)
3347 (branch
3348 TermSpellingDecoded
3349 arrow
3350 .
3351 (nat-eliminate
3352 (lambda unrestricted matched : Nat . (family DoStepDecodeResult))
3353 (constructor DoStepDecodeResult DoStepDecodeFailed)
3354 (lambda unrestricted predecessor : Nat .
3355 (lambda unrestricted induction : (family DoStepDecodeResult) .
3356 (eliminate
3357 TermList
3358 (lambda unrestricted value : (family TermList) .
3359 (family DoStepDecodeResult))
3360 afterArrow
3361 (branch TermListEnd . (constructor DoStepDecodeResult DoStepDecodeFailed))
3362 (branch
3363 TermListNext
3364 computation
3365 rest
3366 ih_rest
3367 .
3368 (eliminate
3369 TermList
3370 (lambda unrestricted value : (family TermList) .
3371 (family DoStepDecodeResult))
3372 rest
3373 (branch
3374 TermListEnd
3375 .
3376 (constructor
3377 DoStepDecodeResult
3378 DoStepDecoded
3379 (succ zero)
3380 quantity
3381 binder
3382 computation))
3383 (branch
3384 TermListNext
3385 extra
3386 tail
3387 ih_tail
3388 .
3389 (constructor DoStepDecodeResult DoStepDecodeFailed)))))))
3390 (bytesEqual arrow leftArrowSpelling)))
3391 (branch TermHasNoSpelling . (constructor DoStepDecodeResult DoStepDecodeFailed))))))))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.