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)
See also must-fail.
(must-succeed form [:with-output-off items] ;; default: :all [:check-expansion bool] )
(must-succeed (assign foo 5)) ;; works fine (@ foo) ;; 5
See the make-event documentation for details.
with-output-off. By default, all output from
(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
Also see must-succeed!.