3671def decodeBinderAfterName =
3672 (lambda unrestricted formTag : Nat .
3673 (lambda unrestricted quantityTag : Nat .
3674 (lambda unrestricted binderSpelling : Bytes .
3675 (lambda unrestricted remaining : (family TermList) .
3676 (eliminate
3677 TermList
3678 (lambda unrestricted value : (family TermList) . (family TermDecodeResult))
3679 remaining
3680 (branch TermListEnd . (binderDecodeFailed binderSyntaxFailureCode))
3681 (branch
3682 TermListNext
3683 colonTerm
3684 afterColon
3685 ih_afterColon
3686 .
3687 (eliminate
3688 TermSpellingResult
3689 (lambda unrestricted result : (family TermSpellingResult) .
3690 (family TermDecodeResult))
3691 (termSpelling colonTerm)
3692 (branch
3693 TermSpellingDecoded
3694 punctuationSpelling
3695 .
3696 (nat-eliminate
3697 (lambda unrestricted matched : Nat . (family TermDecodeResult))
3698 (binderDecodeFailed binderSyntaxFailureCode)
3699 (lambda unrestricted predecessor : Nat .
3700 (lambda unrestricted induction : (family TermDecodeResult) .
3701 (decodeBinderAfterColon formTag quantityTag binderSpelling afterColon)))
3702 (bytesEqual punctuationSpelling colonSpelling)))
3703 (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.