On this page:
assert$
defaxiom
deflabel
defstub
deftheory
defthm
in-theory
mutual-recursion
theory-invariant
defconst
defun
declare
Version: 4.1

2.3 Events and Definitions

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.

Examples:

  > (assert$ (< 0 1) t)

  t

  > (assert$ (< 1 0) t)

  assert$: Assertion failed! stx

(defaxiom name term :rule-classes rule-classes :doc doc-string)

Defines an axiom. Using defaxiom is not recommended.

Examples:

  > (defaxiom sbar (equal t nil)

              :rule-classes nil

              :doc ":Doc-Section ...")

(deflabel name :doc doc-string)

Defines a label, for adding a landmark and/or adding a documentation topic.

Examples:

  > (deflabel interp-section

              :doc ":Doc-Section ...")

(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)

Examples:

  > (deftheory interp-theory

               (set-difference-theories

                 (universal-theory :here)

                 (universal-theory 'interp-section)))

(defthm name term

:rule-classes rule-classes

:instructions instructions

:hints        hints

:otf-flg      otf-flg

:doc          doc-string)

Defines a theorem to be proved and named.

Examples:

  > (defthm x+x=2x (= (+ x x) (* 2 x)))

(in-theory term :doc doc-string)

Examples:

  > (in-theory (set-difference-theories

                 (universal-theory :here)

                 '(flatten (:executable-counterpart flatten))))

(include-book file options ...)

Imports reusable definitions to the current program. See the section on Books and Teachpacks for details on include-book in Dracula.

(mutual-recursion def1 ... defn)

For defining mutually-recursive functions.

Examples:

  > (mutual-recursion

     (defun evenlp (x)

       (if (consp x) (oddlp (cdr x)) t))

     (defun oddlp (x)

       (if (consp x) (evenlp (cdr x)) nil)))

(theory-invariant term :key key :error t/nil)

(defconst name val)

Defines a constant value. The name must begin and end with asterisks.

Examples:

  > (defconst *PI* 22/7)

  > (* 2 *PI*)

  44/7

(defun name (args) (declare decl ...) ... body)

Defines a function.

Examples:

  > (defun absolute-value (x)

         (cond

           ((< x 0) (* -1 x))

           (t x)))

  > (absolute-value 5)

  5

  > (absolute-value -5)

  5

(declare d ...)

Used in defun to give ACL2 extra information about a function.