AlphaGitHub
Source/Packages

Compiler.Parser

packages/compiler/src/Compiler/Parser.alpha

5,902 lines337 declarations199.2 KiBSHA-256 6d135c41813d
Download exact fileView at revisionf5034773ad4bb52133

def · lines 3057–3074

decodeLocalLetBindingTail

Full file
3057def decodeLocalLetBindingTail =
3058  (lambda unrestricted quantity : Nat .
3059    (lambda unrestricted binder : Bytes .
3060      (lambda unrestricted punctuation : Bytes .
3061        (lambda unrestricted terms : (family TermList) .
3062          (nat-eliminate
3063            (lambda unrestricted matched : Nat . (family LocalLetBindingDecodeResult))
3064            (nat-eliminate
3065              (lambda unrestricted matchedColon : Nat . (family LocalLetBindingDecodeResult))
3066              (constructor LocalLetBindingDecodeResult LocalLetBindingDecodeFailed)
3067              (lambda unrestricted predecessor : Nat .
3068                (lambda unrestricted induction : (family LocalLetBindingDecodeResult) .
3069                  (decodeLocalLetAnnotatedTail quantity binder terms)))
3070              (bytesEqual punctuation colonSpelling))
3071            (lambda unrestricted predecessor : Nat .
3072              (lambda unrestricted induction : (family LocalLetBindingDecodeResult) .
3073                (decodeLocalLetInferredTail quantity binder terms)))
3074            (bytesEqual punctuation equalsSpelling))))))

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.