Sharp-d-reader
Read a rational number as a representable rational (see df)
When the ACL2 reader encounters the two-character sequence #d,
it invokes the Lisp reader to obtain the next token, which should designate a
Lisp double-precision floating-point number. (Technically, the Lisp value of
variable *read-default-float-format* is the symbol DOUBLE-FLOAT when
the floating-point token is read.) The reader then returns the rational
number represented by that floating-point token.
The discussion above is complete, but it may make more sense to those
familiar with so-called df values in ACL2. See df.
See also sharp-f-reader, which reads input starting with #f.
As with #d, one reads floating-point notation and returns the
corresponding rational number. However, while #d reads the next token as
a Lisp floating-point number, #f is specific to ACL2 and follows precise
documented rules that, unlike #d, allow use of underscores (_) and
hexadecimal notation.
