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 3299–3325

decodeDoReturn

Full file
3299def decodeDoReturn =
3300  (lambda unrestricted term : (family Term) .
3301    (eliminate
3302      TermApplicationSpine
3303      (lambda unrestricted value : (family TermApplicationSpine) . (family DoBodyDecodeResult))
3304      (termApplicationSpine term)
3305      (branch
3306        TermApplicationSpineValue
3307        head
3308        arguments
3309        .
3310        (eliminate
3311          TermSpellingResult
3312          (lambda unrestricted result : (family TermSpellingResult) . (family DoBodyDecodeResult))
3313          (termSpelling head)
3314          (branch
3315            TermSpellingDecoded
3316            spelling
3317            .
3318            (nat-eliminate
3319              (lambda unrestricted matched : Nat . (family DoBodyDecodeResult))
3320              (constructor DoBodyDecodeResult DoBodyDecodeFailed)
3321              (lambda unrestricted predecessor : Nat .
3322                (lambda unrestricted induction : (family DoBodyDecodeResult) .
3323                  (decodeDoReturnArguments arguments)))
3324              (bytesEqual spelling returnSpelling)))
3325          (branch TermHasNoSpelling . (constructor DoBodyDecodeResult DoBodyDecodeFailed))))))

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.