ACL2s-interface
An interface for interacting with ACL2/ACL2s from Common Lisp.
WARNING: Loading this book by default will result in the
redefinition of comment-window-co. This is unfortunately the only
way we found to control comment-window printing. If you would like to
disable this feature, you can add the
ACL2S-INTERFACE-NO-OVERWRITE feature, e.g. by running (push
:ACL2S-INTERFACE-NO-OVERWRITE *features*) in raw mode before
certifying this book.
Subtopics
- Itest?-query
- Find counterexamples to an ACL2s statement.
- ACL2s-event
- Install an ACL2 event from Common Lisp
- ACL2s-query
- Run a multiple-value ACL2 computation from Common Lisp
- Quiet-mode-hooks
- Hooks that fire when the ACL2s interface quiet mode is turned on or off.
- ACL2s-interface-symbol-package-tips
- Tips for dealing with symbol package issues when using the ACL2s interface
- ACL2s-compute
- Run a single-value ACL2 computation from Common Lisp
- ACL2s-interface::ACL2s-interface-utils
- Some utilities built into the ACL2s interface.
- Quiet-mode
- Control whether or not the acl2s-interface attempts to suppress ACL2 printed output
- Capture-output
- Control whether or not the acl2s-interface attempts to capture ACL2 printed output
