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 2048–2067

integerSpellingLooksNumeric

Full file
2048def integerSpellingLooksNumeric =
2049  (lambda unrestricted spelling : Bytes .
2050    (bytes-eliminate
2051      (lambda unrestricted remaining : Bytes . Nat)
2052      zero
2053      (lambda unrestricted head : Byte .
2054        (lambda unrestricted tail : Bytes .
2055          (lambda unrestricted ignored : Nat .
2056            (nat-eliminate
2057              (lambda unrestricted matchedDigit : Nat . Nat)
2058              (nat-eliminate
2059                (lambda unrestricted matchedMinus : Nat . Nat)
2060                zero
2061                (lambda unrestricted predecessor : Nat .
2062                  (lambda unrestricted induction : Nat . (integerSpellingTailStartsDigit tail)))
2063                (byte-equal head (byte 45)))
2064              (lambda unrestricted predecessor : Nat .
2065                (lambda unrestricted induction : Nat . (succ zero)))
2066              (isDecimalDigit head)))))
2067      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.