		Search-engine friendly clone of the ACL2 documentation.

Must-succeed

A top-level assert$-like command. Ensures that a command which returns an error-triple—e.g., a defun or defthm—will return successfully.

This can be useful for adding simple unit tests of macros, theories, etc. to your books. Basic examples:

(must-succeed                  ;; works fine
  (defun f (x) (consp x)))     ;;   (NOTE: F not defined afterwards!)

(must-succeed                  ;; causes an error
  (defthm bad-theorem nil))    ;;   (unless we can prove NIL!)

(must-succeed                  ;; causes an error
  (set-cbd 17))                ;;   (because 17 isn't a string)

General form:

(must-succeed form
              [:with-output-off items]  ;; default:  :all
              [:check-expansion bool]
              )

The form should evaluate to an error-triple, which is true for most top-level ACL2 events and other high level commands.

The form is submitted in a make-event, which has a number of consequences. Most importantly, when form is an event like a defun, or defthm, it doesn't persist after the must-succeed form. Other state updates do persist, e.g.,

(must-succeed (assign foo 5))   ;; works fine
(@ foo)                         ;; 5

See the make-event documentation for details.

Options

with-output-off. By default, all output from form is suppressed, but you can customize this. Typical example:

(must-succeed
  (defun f (x) (consp x))
  :with-output-off nil)    ;; don't suppress anything

check-expansion. By default the form won't be re-run and re-checked at include-book time. But you can use :check-expansion to customize this, as in make-event.

Also see must-succeed!.

Subtopics

Must-succeed*: A variant of must-succeed that accepts multiple forms.