Major Section: MISCELLANEOUS
ACL2 is a logic, a theorem prover, and a programming language based on Common Lisp. A connection with Common Lisp is established with guards (see guard).
However, here we document potential deviations from Common Lisp semantics even in the presence of verified guards. Our view is that these deviations are extremely unlikely to manifest; indeed, as of this writing we are unaware of any cases in which these issues arise in practice. However, we feel obligated to acknowledge their possibility, which could result in surprises during evaluation or even proof.
nil. However, in ACL2 these functions are assumed to return
t. For details,see generalized-booleans.
The execution of forms with
program mode functions can result in
calls of functions on arguments that do not satisfy their guards. In
practice, this simply causes hard Lisp errors. But in principle one could
imagine a damaged Lisp image that operates incorrectly.
The Common Lisp spec, specifically Section 22.214.171.124 of the Common Lisp
HyperSpec, allows for undefined results when a function is ``multiply
defined'' in a compiled file. ACL2 allows redundant
defuns in a book,
and in general books are compiled by
see compilation for an exception). Moreover, ACL2 provides a redefinition
capability (see ld-redefinition-action and see redef), and the above
section also allows for undefined results when a function is defined in a
compiled file and then redefined, presumably (for example) because of