2924def decodeLocalLetAnnotatedTail =
2925 (lambda unrestricted quantity : Nat .
2926 (lambda unrestricted binder : Bytes .
2927 (lambda unrestricted terms : (family TermList) .
2928 (eliminate
2929 TermList
2930 (lambda unrestricted value : (family TermList) . (family LocalLetBindingDecodeResult))
2931 terms
2932 (branch
2933 TermListEnd
2934 .
2935 (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed))
2936 (branch
2937 TermListNext
2938 annotation
2939 afterAnnotation
2940 ih_afterAnnotation
2941 .
2942 (eliminate
2943 TermList
2944 (lambda unrestricted value : (family TermList) . (family LocalLetBindingDecodeResult))
2945 afterAnnotation
2946 (branch
2947 TermListEnd
2948 .
2949 (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed))
2950 (branch
2951 TermListNext
2952 equalsTerm
2953 afterEquals
2954 ih_afterEquals
2955 .
2956 (eliminate
2957 TermSpellingResult
2958 (lambda unrestricted result : (family TermSpellingResult) .
2959 (family LocalLetBindingDecodeResult))
2960 (termSpelling equalsTerm)
2961 (branch
2962 TermSpellingDecoded
2963 spelling
2964 .
2965 (nat-eliminate
2966 (lambda unrestricted matched : Nat . (family LocalLetBindingDecodeResult))
2967 (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed)
2968 (lambda unrestricted predecessor : Nat .
2969 (lambda unrestricted induction : (family LocalLetBindingDecodeResult) .
2970 (eliminate
2971 TermList
2972 (lambda unrestricted value : (family TermList) .
2973 (family LocalLetBindingDecodeResult))
2974 afterEquals
2975 (branch
2976 TermListEnd
2977 .
2978 (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed))
2979 (branch
2980 TermListNext
2981 value
2982 rest
2983 ih_rest
2984 .
2985 (eliminate
2986 TermList
2987 (lambda unrestricted value : (family TermList) .
2988 (family LocalLetBindingDecodeResult))
2989 rest
2990 (branch
2991 TermListEnd
2992 .
2993 (constructor
2994 LocalLetBindingDecodeResult
2995 LocalLetBindingDecoded
2996 quantity
2997 binder
2998 (succ zero)
2999 annotation
3000 value))
3001 (branch
3002 TermListNext
3003 extra
3004 tail
3005 ih_tail
3006 .
3007 (constructor
3008 LocalLetBindingDecodeResult
3009 LocalLetBindingDecodeFailed)))))))
3010 (bytesEqual spelling equalsSpelling)))
3011 (branch
3012 TermHasNoSpelling
3013 .
3014 (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.