3618def decodeBinderAfterDomain =
3619 (lambda unrestricted formTag : Nat .
3620 (lambda unrestricted quantityTag : Nat .
3621 (lambda unrestricted binderSpelling : Bytes .
3622 (lambda unrestricted domain : (family Term) .
3623 (lambda unrestricted remaining : (family TermList) .
3624 (eliminate
3625 TermList
3626 (lambda unrestricted value : (family TermList) . (family TermDecodeResult))
3627 remaining
3628 (branch TermListEnd . (binderDecodeFailed binderSyntaxFailureCode))
3629 (branch
3630 TermListNext
3631 dotTerm
3632 afterDot
3633 ih_afterDot
3634 .
3635 (eliminate
3636 TermSpellingResult
3637 (lambda unrestricted result : (family TermSpellingResult) .
3638 (family TermDecodeResult))
3639 (termSpelling dotTerm)
3640 (branch
3641 TermSpellingDecoded
3642 punctuationSpelling
3643 .
3644 (nat-eliminate
3645 (lambda unrestricted matched : Nat . (family TermDecodeResult))
3646 (binderDecodeFailed binderSyntaxFailureCode)
3647 (lambda unrestricted predecessor : Nat .
3648 (lambda unrestricted induction : (family TermDecodeResult) .
3649 (decodeBinderAfterDot formTag quantityTag binderSpelling domain afterDot)))
3650 (bytesEqual punctuationSpelling dotSpelling)))
3651 (branch TermHasNoSpelling . (binderDecodeFailed binderSyntaxFailureCode))))))))))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.