ACL2-sedan
ACL2 Sedan interface
Many successful ACL2 users run in a shell under Emacs; see emacs. However, those not familiar with Emacs may prefer to start with an
Eclipse-based interface initially developed by Peter Dillinger and Pete
Manolios called the ACL2 Sedan or ``ACL2s''.
ACL2 sessions in the ACL2 Sedan can utilize non-standard extensions and
enhancements, especially geared toward new users, termination reasoning, and
attaching rich user interfaces. These extensions are distributed with the
ACL2 community books in books/acl2s/distribution/acl2s-hooks/. Thanks to
Peter Dillinger, Pete Manolios, Daron Vroon, and Harsh Raju Chamarthi for
their work on the ACL2 Sedan and for making their books available to ACL2
users.
Subtopics
- Defunc
- Function definitions with contracts. See also
definec and defun.
- Cgen
- Counterexample Generation a.k.a Disproving for ACL2
- Ccg
- A powerful automated termination prover for ACL2
- Defdata
- A Data Definition Framework
- ACL2s-user-guide
- ACL2 Sedan User Guide
- ACL2s-tutorial
- A short ACL2s tutorial
- ACL2s-implementation-notes
- Some details regarding how ACL2s is implemented
- Match
- Pattern matching supporting predicates, including
recognizers automatically generated by defdata,
disjunctive patterns and patterns containing arbitrary code.
Can be thought of as ACL2s version of case-match.
- ACL2s-faq
- Frequently Asked Questions
- ACL2s-intro
- A longer introduction to ACL2s
- ACL2s-defaults
- Getting and setting defaults for various parameters in Cgen (ACL2 Sedan)
- Definec
- Function definitions with contracts extending defunc.
- ACL2s-utilities
- Utilities used in ACL2s.
- ACL2s-interface
- An interface for interacting with ACL2/ACL2s from Common Lisp.
- ACL2s-installation
- Describes how to install ACL2s
