|
|
|---|
|
|
|
|---|
Floating-point and ACL2
ACL2 supports computation that uses floating-point operations; see
df. If you are using an older Lisp, an attempt to build ACL2 may fail
with an error complaining that “feature :ieee-floating-point is
missing from *features*”. If you believe that your host Lisp
properly supports IEEE floating-point operations even though that feature is
missing (e.g., quite possibly with older versions of CCL), you can avoid that
built-time error by setting environment variable