3869def decodeTermEliminatorBranchMembers =
3870 (lambda unrestricted members : (family TermList) .
3871 (eliminate
3872 TermList
3873 (lambda unrestricted value : (family TermList) .
3874 (pi unrestricted constructorName : Bytes .
3875 (pi unrestricted reversedBinders : (family Term) . (family TermDecodeResult))))
3876 members
3877 (branch
3878 TermListEnd
3879 .
3880 (lambda unrestricted constructorName : Bytes .
3881 (lambda unrestricted reversedBinders : (family Term) . familyTermDecodeFailed)))
3882 (branch
3883 TermListNext
3884 member
3885 remaining
3886 ih_remaining
3887 .
3888 (lambda unrestricted constructorName : Bytes .
3889 (lambda unrestricted reversedBinders : (family Term) .
3890 (eliminate
3891 TermSpellingResult
3892 (lambda unrestricted result : (family TermSpellingResult) . (family TermDecodeResult))
3893 (termSpelling member)
3894 (branch
3895 TermSpellingDecoded
3896 spelling
3897 .
3898 (nat-eliminate
3899 (lambda unrestricted matchedDot : Nat . (family TermDecodeResult))
3900 (ih_remaining
3901 constructorName
3902 (constructor Term TermSequenceNext member reversedBinders))
3903 (lambda unrestricted predecessor : Nat .
3904 (lambda unrestricted induction : (family TermDecodeResult) .
3905 (finishTermEliminatorBranch constructorName reversedBinders remaining)))
3906 (bytesEqual spelling dotSpelling)))
3907 (branch TermHasNoSpelling . familyTermDecodeFailed)))))))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.