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 1840–1857

sourceByteFromTerm

Full file
1840def sourceByteFromTerm =
1841  (lambda unrestricted term : (family Term) .
1842    (eliminate
1843      NaturalTermResult
1844      (lambda unrestricted result : (family NaturalTermResult) . (family SourceByteResult))
1845      (naturalValueFromTerm term)
1846      (branch
1847        NaturalTermDecoded
1848        naturalTermValue
1849        .
1850        (nat-eliminate
1851          (lambda unrestricted fits : Nat . (family SourceByteResult))
1852          (constructor SourceByteResult SourceByteInvalid)
1853          (lambda unrestricted predecessor : Nat .
1854            (lambda unrestricted induction : (family SourceByteResult) .
1855              (constructor SourceByteResult SourceByteDecoded (nat-to-byte naturalTermValue))))
1856          (naturalLessThan naturalTermValue byteModulus)))
1857      (branch NotNaturalTerm . (constructor SourceByteResult SourceByteInvalid))))

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.