Source/Packages

Compiler.Parser

packages/compiler/src/Compiler/Parser.alpha

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

def · lines 3599–3616

decodeBinderAfterDot

Full file
3599def decodeBinderAfterDot =
3600  (lambda unrestricted formTag : Nat .
3601    (lambda unrestricted quantityTag : Nat .
3602      (lambda unrestricted binderSpelling : Bytes .
3603        (lambda unrestricted domain : (family Term) .
3604          (lambda unrestricted remaining : (family TermList) .
3605            (eliminate
3606              TermList
3607              (lambda unrestricted value : (family TermList) . (family TermDecodeResult))
3608              remaining
3609              (branch TermListEnd . (binderDecodeFailed binderSyntaxFailureCode))
3610              (branch
3611                TermListNext
3612                body
3613                bodyRest
3614                ih_bodyRest
3615                .
3616                (finishBinderForm formTag quantityTag binderSpelling domain body bodyRest))))))))

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.