3076def decodeLocalLetBindingArguments =
3077 (lambda unrestricted quantity : Nat .
3078 (lambda unrestricted arguments : (family TermList) .
3079 (eliminate
3080 TermList
3081 (lambda unrestricted value : (family TermList) . (family LocalLetBindingDecodeResult))
3082 arguments
3083 (branch TermListEnd . (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed))
3084 (branch
3085 TermListNext
3086 binderTerm
3087 afterBinder
3088 ih_afterBinder
3089 .
3090 (eliminate
3091 TermSpellingResult
3092 (lambda unrestricted result : (family TermSpellingResult) .
3093 (family LocalLetBindingDecodeResult))
3094 (termSpelling binderTerm)
3095 (branch
3096 TermSpellingDecoded
3097 binder
3098 .
3099 (eliminate
3100 TermList
3101 (lambda unrestricted value : (family TermList) .
3102 (family LocalLetBindingDecodeResult))
3103 afterBinder
3104 (branch
3105 TermListEnd
3106 .
3107 (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed))
3108 (branch
3109 TermListNext
3110 punctuationTerm
3111 terms
3112 ih_terms
3113 .
3114 (eliminate
3115 TermSpellingResult
3116 (lambda unrestricted result : (family TermSpellingResult) .
3117 (family LocalLetBindingDecodeResult))
3118 (termSpelling punctuationTerm)
3119 (branch
3120 TermSpellingDecoded
3121 punctuation
3122 .
3123 (decodeLocalLetBindingTail quantity binder punctuation terms))
3124 (branch
3125 TermHasNoSpelling
3126 .
3127 (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed))))))
3128 (branch
3129 TermHasNoSpelling
3130 .
3131 (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed)))))))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.