must-prove

(in-package "ACL2")

(defsection must-prove
  :parents (std/testing errors)
  :short "A top-level @(tsee assert$)-like command to ensure that
          a formula gets proved."
  :long "<p>This takes the same arguments as @(tsee thm).
   It wraps the @(tsee thm) into a @(tsee must-succeed).</p>

   @(def must-prove)"
  (defmacro must-prove
    (&rest args)
    `(must-succeed (thm ,@ARGS))))