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 5194–5212

prependDecodedSequence

Full file
5194def prependDecodedSequence =
5195  (lambda unrestricted head : (family Term) .
5196    (lambda unrestricted tail : (family TermList) .
5197      (eliminate
5198        TermSpellingResult
5199        (lambda unrestricted value : (family TermSpellingResult) . (family TermList))
5200        (termSpelling head)
5201        (branch
5202          TermSpellingDecoded
5203          spelling
5204          .
5205          (nat-eliminate
5206            (lambda unrestricted match : Nat . (family TermList))
5207            (constructor TermList TermListNext head tail)
5208            (lambda unrestricted predecessor : Nat .
5209              (lambda unrestricted induction : (family TermList) .
5210                (prependUniverseSequence head tail)))
5211            (bytesEqual spelling universeTypeSpelling)))
5212        (branch TermHasNoSpelling . (constructor TermList TermListNext head tail)))))

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.