Inspect only the first byte. This keeps the empty/nonempty decision
bounded instead of materializing bytes-length as a second unary traversal
before the checked digit fold.
824def integerLiteralHasDigits =
825 (lambda unrestricted digits : Bytes .
826 (bytes-eliminate
827 (lambda unrestricted remaining : Bytes . Nat)
828 zero
829 (lambda unrestricted head : Byte .
830 (lambda unrestricted tail : Bytes . (lambda unrestricted continue : Nat . (succ zero))))
831 digits))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.