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.