343def integerLiteralDecodeDecimal =
344 (lambda unrestricted value : Byte .
345 (nat-eliminate
346 (lambda unrestricted current : Nat . (family IntegerLiteralDigitResult))
347 integerLiteralBadDigitResult
348 (lambda unrestricted predecessor : Nat .
349 (lambda unrestricted induction : (family IntegerLiteralDigitResult) .
350 (nat-eliminate
351 (lambda unrestricted current : Nat . (family IntegerLiteralDigitResult))
352 integerLiteralBadDigitResult
353 (lambda unrestricted predecessorAgain : Nat .
354 (lambda unrestricted inductionAgain : (family IntegerLiteralDigitResult) .
355 (constructor
356 IntegerLiteralDigitResult
357 IntegerLiteralDigitValue
358 (naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 48))))))
359 (byte-less-than value (byte 58)))))
360 (byte-less-than (byte 47) value)))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.