Source/Packages

Compiler.Parser

packages/compiler/src/Compiler/Parser.alpha

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

def · lines 3926–3960

decodeEliminatorAfterFamily

Full file
3926def decodeEliminatorAfterFamily =
3927  (lambda unrestricted familyName : Bytes .
3928    (lambda unrestricted remaining : (family TermList) .
3929      (eliminate
3930        TermList
3931        (lambda unrestricted value : (family TermList) . (family TermDecodeResult))
3932        remaining
3933        (branch TermListEnd . familyTermDecodeFailed)
3934        (branch
3935          TermListNext
3936          motive
3937          afterMotive
3938          ih_afterMotive
3939          .
3940          (eliminate
3941            TermList
3942            (lambda unrestricted value : (family TermList) . (family TermDecodeResult))
3943            afterMotive
3944            (branch TermListEnd . familyTermDecodeFailed)
3945            (branch
3946              TermListNext
3947              scrutinee
3948              branches
3949              ih_branches
3950              .
3951              (constructor
3952                TermDecodeResult
3953                TermDecoded
3954                (constructor
3955                  Term
3956                  Eliminator
3957                  familyName
3958                  motive
3959                  scrutinee
3960                  (termListToTermSequence branches)))))))))

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.