ACL2-sedan
ACL2 Sedan interface
Many successful ACL2 users run in an 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 generally
available as certifiable ACL2 books.
(Some code originating from this project has been migrated to the ACL2
community books, but only after it was quite stable.) 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
- ACL2s-faq
- Frequently Asked Questions
- 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-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-installation
- Describes how to install ACL2s
