Source/Packages

Compiler.Parser

packages/compiler/src/Compiler/Parser.alpha

5,902 lines337 declarations199.2 KiBSHA-256 6d135c41813d

def · lines 3237–3268

decodeLocalLetSequence

Full file
3237def decodeLocalLetSequence =
3238  (lambda unrestricted terms : (family TermList) .
3239    (eliminate
3240      TermList
3241      (lambda unrestricted value : (family TermList) . (family TermDecodeResult))
3242      terms
3243      (branch TermListEnd . localLetSyntaxFailure)
3244      (branch
3245        TermListNext
3246        head
3247        rest
3248        ih_rest
3249        .
3250        (eliminate
3251          TermSpellingResult
3252          (lambda unrestricted result : (family TermSpellingResult) . (family TermDecodeResult))
3253          (termSpelling head)
3254          (branch
3255            TermSpellingDecoded
3256            spelling
3257            .
3258            (nat-eliminate
3259              (lambda unrestricted matched : Nat . (family TermDecodeResult))
3260              (finishDecodedLocalLetBinding ih_rest (decodeLocalLetBinding head))
3261              (lambda unrestricted predecessor : Nat .
3262                (lambda unrestricted induction : (family TermDecodeResult) .
3263                  (decodeLocalLetAfterIn rest)))
3264              (bytesEqual spelling inSpelling)))
3265          (branch
3266            TermHasNoSpelling
3267            .
3268            (finishDecodedLocalLetBinding ih_rest (decodeLocalLetBinding head)))))))

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.