ACL2 events are special terms which define new functions or logical rules. Defined names are in scope within their own definition and below; forward references are not allowed. Use the mutual-recursion event for mutually recursive functions.
|(assert$ test form)|
Raises an error if the given test fails.
|> (assert$ (< 0 1) t)|
|> (assert$ (< 1 0) t)|
|(defaxiom name term :rule-classes rule-classes :doc doc-string)|
Defines an axiom. Using defaxiom is not recommended.
|(deflabel name :doc doc-string)|
Defines a label, for adding a landmark and/or adding a documentation topic.
|(defstub name args-sig => output-sig :doc doc-string)|
|(deftheory name term :doc doc-string)|
Defines a theory (to enable or disable a set of rules)
Defines a theorem to be proved and named.
|> (defthm x+x=2x (= (+ x x) (* 2 x)))|
|(in-theory term :doc doc-string)|
|(include-book "<basename>" :dir :system)|
|(include-book "<basename>" :dir :teachpacks)|
The include-book form imports definitions from a file called a book. Dracula supports three variants.
Without a :dir option, Dracula adds a ".lisp" extension to the base name and attempts to load a file relative to the current directory. In the case above, the program must reside in a directory with a "my-path" subdirectory containing a book named "my-book.lisp".
Books must be valid Dracula programs; they must start with (in-package "ACL2"); and they must contain only events, no top-level expressions.
(include-book "my-path/my-book" :dir :system)
This variant loads a book from the system directory included with an ACL2 installation. Dracula simulates only a couple of the definitions from these books, but allows other books to be included for theorem proving purposes. See ACL2 Books for the list of books supported by Dracula.
(include-book "my-path/my-book" :dir :teachpack)
The third variant loads one of the books provided with Dracula, called teachpacks. These books make use of DrScheme features such as interactive animations and other i/o, and are also reflected in the ACL2 logic. See Teachpacks for the list of provided teachpacks.
|(mutual-recursion def1 defn)|
For defining mutually-recursive functions.
|(theory-invariant term :key key :error t/nil)|
|(defconst name val)|
Defines a constant value. The name must begin and end with asterisks.
|> (defconst *PI* 22/7)|
|> (* 2 *PI*)|
|(defun name (args) (declare decl ) body)|
Defines a function.
|> (absolute-value 5)|
|> (absolute-value -5)|
|(declare d )|
Used in defun to give ACL2 extra information about a function.
Declares pred to be an equivalence predicate. It is equivalent to the following, with the supplied name substituted for pred in all identifiers:
|(and (booleanp (pred x y))|
|(pred x x)|
|(implies (pred x y) (pred y x))|
|(implies (and (pred x y)|
|(pred y z))|
|(pred x z)))|