Source/Packages

Compiler.Parser

packages/compiler/src/Compiler/Parser.alpha

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

def · lines 2069–2092

decodeUnquotedAtom

Full file
2069def decodeUnquotedAtom =
2070  (lambda unrestricted spelling : Bytes .
2071    (chooseDecodedAtom
2072      (bytesEqual spelling zeroSpelling)
2073      (constructor Term NaturalZero)
2074      (chooseDecodedAtom
2075        (bytesEqual spelling naturalTypeSpelling)
2076        (constructor Term NaturalType)
2077        (chooseDecodedAtom
2078          (bytesEqual spelling bytesTypeSpelling)
2079          (constructor Term BytesType)
2080          (chooseDecodedAtom
2081            (bytesEqual spelling byteTypeSpelling)
2082            (constructor Term ByteType)
2083            (nat-eliminate
2084              (lambda unrestricted matched : Nat . (family TermDecodeResult))
2085              (constructor TermDecodeResult TermDecoded (constructor Term Variable spelling))
2086              (lambda unrestricted predecessor : Nat .
2087                (lambda unrestricted induction : (family TermDecodeResult) .
2088                  (constructor
2089                    TermDecodeResult
2090                    TermDecoded
2091                    (constructor Term IntegerLiteral spelling))))
2092              (integerSpellingLooksNumeric 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.