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 3741–3754

decodeBinderForm

Full file
3741def decodeBinderForm =
3742  (lambda unrestricted formTag : Nat .
3743    (lambda unrestricted quantityTerm : (family Term) .
3744      (lambda unrestricted remaining : (family TermList) .
3745        (eliminate
3746          TermSpellingResult
3747          (lambda unrestricted result : (family TermSpellingResult) . (family TermDecodeResult))
3748          (termSpelling quantityTerm)
3749          (branch
3750            TermSpellingDecoded
3751            quantitySpelling
3752            .
3753            (decodeBinderQuantity formTag (decodeQuantitySpelling quantitySpelling) remaining))
3754          (branch TermHasNoSpelling . (binderDecodeFailed binderSyntaxFailureCode))))))

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.