SHARP-U-READER

allow underscore characters in numbers
Major Section:  OTHER

Example:

ACL2 !>#ub1000_1000_1000_
2184
ACL2 !>#b100010001000
2184
ACL2 !>#uo1_1
9
ACL2 !>#o11
9
ACL2 !>#u34_5
345
ACL2 !>#u345
345
ACL2 !>345
345
ACL2 !>#ux12_a
298
ACL2 !>#ux12a
298
ACL2 !>#u x12a
298
ACL2 !>#x12a
298
ACL2 !>#u123_456/7_919
123456/7919
ACL2 !>

The ACL2 reader supports the use of #ub, #uo, and #ux where one would otherwise write #b, #o, and #x, respectively (for binary, octal, and hexadecimal numerals), but where underscore characters (`_') are allowed but ignored. Also supported is the prefix #u in front of a an expression that is a decimal numeral except that underscore characteres are allowed but ignored.

The precise specification of #u is as follows. The Lisp reader reads one expression after the #u. If the result is a number, then that number is returned by the reader. Otherwise the result must be a symbol whose name begins with one of the characters `B', `O', or `X', or else a decimal digit (one of the characters `0, 1, ..., 9'). All underscores are removed from the name of that symbol to obtain a string and in the first three cases only, a `#' character is prepended to that string. The resulting string is then handed to the Lisp reader in order to obtain the final result, which must be a number or else an error occurs.