Source/Packages

Compiler.IntegerLiteral

packages/compiler/src/Compiler/IntegerLiteral.alpha

903 lines95 declarations31.8 KiBSHA-256 578f5c4899f4

def · lines 546–554

integerLiteralDigitValid

Full file
A separator has a valid radix digit on both sides. The continuation carries only that preceding-digit fact; arithmetic starts after validation.
546def integerLiteralDigitValid =
547  (lambda unrestricted radix : (family IntegerLiteralRadix) .
548    (lambda unrestricted value : Byte .
549      (eliminate
550        IntegerLiteralDigitResult
551        (lambda unrestricted current : (family IntegerLiteralDigitResult) . Nat)
552        (integerLiteralDecodeDigit radix value)
553        (branch IntegerLiteralDigitValue digit . (succ zero))
554        (branch IntegerLiteralDigitFailed failure . zero))))

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.