Source/Packages

Compiler.Parser

packages/compiler/src/Compiler/Parser.alpha

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

def · lines 3393–3412

decodeDoLongNamed

Full file
3393def decodeDoLongNamed =
3394  (lambda unrestricted quantity : Nat .
3395    (lambda unrestricted arguments : (family TermList) .
3396      (eliminate
3397        TermList
3398        (lambda unrestricted value : (family TermList) . (family DoStepDecodeResult))
3399        arguments
3400        (branch TermListEnd . (constructor DoStepDecodeResult DoStepDecodeFailed))
3401        (branch
3402          TermListNext
3403          binderTerm
3404          rest
3405          ih_rest
3406          .
3407          (eliminate
3408            TermSpellingResult
3409            (lambda unrestricted result : (family TermSpellingResult) . (family DoStepDecodeResult))
3410            (termSpelling binderTerm)
3411            (branch TermSpellingDecoded binder . (decodeDoNamedTail quantity binder rest))
3412            (branch TermHasNoSpelling . (constructor DoStepDecodeResult DoStepDecodeFailed)))))))

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.