362def integerLiteralDecodeBinary =
363 (lambda unrestricted value : Byte .
364 (nat-eliminate
365 (lambda unrestricted current : Nat . (family IntegerLiteralDigitResult))
366 integerLiteralBadDigitResult
367 (lambda unrestricted predecessor : Nat .
368 (lambda unrestricted induction : (family IntegerLiteralDigitResult) .
369 (nat-eliminate
370 (lambda unrestricted current : Nat . (family IntegerLiteralDigitResult))
371 integerLiteralBadDigitResult
372 (lambda unrestricted predecessorAgain : Nat .
373 (lambda unrestricted inductionAgain : (family IntegerLiteralDigitResult) .
374 (constructor
375 IntegerLiteralDigitResult
376 IntegerLiteralDigitValue
377 (naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 48))))))
378 (byte-less-than value (byte 50)))))
379 (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.