3016def decodeLocalLetInferredTail =
3017 (lambda unrestricted quantity : Nat .
3018 (lambda unrestricted binder : Bytes .
3019 (lambda unrestricted terms : (family TermList) .
3020 (eliminate
3021 TermList
3022 (lambda unrestricted value : (family TermList) . (family LocalLetBindingDecodeResult))
3023 terms
3024 (branch
3025 TermListEnd
3026 .
3027 (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed))
3028 (branch
3029 TermListNext
3030 value
3031 rest
3032 ih_rest
3033 .
3034 (eliminate
3035 TermList
3036 (lambda unrestricted value : (family TermList) . (family LocalLetBindingDecodeResult))
3037 rest
3038 (branch
3039 TermListEnd
3040 .
3041 (constructor
3042 LocalLetBindingDecodeResult
3043 LocalLetBindingDecoded
3044 quantity
3045 binder
3046 zero
3047 (constructor Term NaturalType)
3048 value))
3049 (branch
3050 TermListNext
3051 extra
3052 tail
3053 ih_tail
3054 .
3055 (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.