3393def decodeDoLongNamed =
3394 (lambda unrestricted quantity : Nat .
3395 (lambda unrestricted arguments : (family TermList) .
3396 (eliminate
3397 TermList
3398 (lambda unrestricted value : (family TermList) . (family DoStepDecodeResult))
3399 arguments
3400 (branch TermListEnd . (constructor DoStepDecodeResult DoStepDecodeFailed))
3401 (branch
3402 TermListNext
3403 binderTerm
3404 rest
3405 ih_rest
3406 .
3407 (eliminate
3408 TermSpellingResult
3409 (lambda unrestricted result : (family TermSpellingResult) . (family DoStepDecodeResult))
3410 (termSpelling binderTerm)
3411 (branch TermSpellingDecoded binder . (decodeDoNamedTail quantity binder rest))
3412 (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.