56def isDecimalDigit =
57 (lambda unrestricted byte : Byte .
58 (nat-eliminate
59 (lambda unrestricted belowLowerBound : Nat . Nat)
60 (nat-eliminate
61 (lambda unrestricted belowUpperBound : Nat . Nat)
62 zero
63 (lambda unrestricted predecessor : Nat .
64 (lambda unrestricted induction : Nat . (succ zero)))
65 (byte-less-than byte (byte 58)))
66 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
67 (byte-less-than byte (byte 48))))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.