3133def decodeLocalLetBinding =
3134 (lambda unrestricted term : (family Term) .
3135 (eliminate
3136 TermApplicationSpine
3137 (lambda unrestricted value : (family TermApplicationSpine) .
3138 (family LocalLetBindingDecodeResult))
3139 (termApplicationSpine term)
3140 (branch
3141 TermApplicationSpineValue
3142 head
3143 arguments
3144 .
3145 (eliminate
3146 TermSpellingResult
3147 (lambda unrestricted result : (family TermSpellingResult) .
3148 (family LocalLetBindingDecodeResult))
3149 (termSpelling head)
3150 (branch
3151 TermSpellingDecoded
3152 quantitySpelling
3153 .
3154 (eliminate
3155 QuantityDecodeResult
3156 (lambda unrestricted result : (family QuantityDecodeResult) .
3157 (family LocalLetBindingDecodeResult))
3158 (decodeQuantitySpelling quantitySpelling)
3159 (branch
3160 QuantityDecoded
3161 quantity
3162 .
3163 (decodeLocalLetBindingArguments quantity arguments))
3164 (branch
3165 QuantityInvalid
3166 .
3167 (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed))))
3168 (branch
3169 TermHasNoSpelling
3170 .
3171 (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.