Source/Packages

Compiler.Parser

packages/compiler/src/Compiler/Parser.alpha

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

def · lines 1571–1598

parseUnsignedNaturalLiteral

Full file
1571def parseUnsignedNaturalLiteral =
1572  (lambda unrestricted spelling : Bytes .
1573    (chooseNaturalLiteralParse
1574      (byte-equal (bytes-head spelling) (byte 48))
1575      (lambda unrestricted force : Nat .
1576        (chooseNaturalLiteralParse
1577          (addNatural
1578            (byte-equal (bytes-head (bytes-tail spelling)) (byte 120))
1579            (byte-equal (bytes-head (bytes-tail spelling)) (byte 88)))
1580          (lambda unrestricted force : Nat .
1581            (parseNaturalLiteralDigits
1582              (constructor IntegerLiteralRadix IntegerLiteralHexadecimal)
1583              (bytes-tail (bytes-tail spelling))))
1584          (lambda unrestricted force : Nat .
1585            (chooseNaturalLiteralParse
1586              (addNatural
1587                (byte-equal (bytes-head (bytes-tail spelling)) (byte 98))
1588                (byte-equal (bytes-head (bytes-tail spelling)) (byte 66)))
1589              (lambda unrestricted force : Nat .
1590                (parseNaturalLiteralDigits
1591                  (constructor IntegerLiteralRadix IntegerLiteralBinary)
1592                  (bytes-tail (bytes-tail spelling))))
1593              (lambda unrestricted force : Nat .
1594                (parseNaturalLiteralDigits
1595                  (constructor IntegerLiteralRadix IntegerLiteralDecimal)
1596                  spelling))))))
1597      (lambda unrestricted force : Nat .
1598        (parseNaturalLiteralDigits (constructor IntegerLiteralRadix IntegerLiteralDecimal) spelling))))

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.