must-be-redundant

(in-package "ACL2")

(defsection must-be-redundant
  :parents (std/testing errors)
  :short "A top-level @(tsee assert$)-like command
          to ensure that given forms are redundant."
  :long "<p>The forms are put into an @(tsee encapsulate),
   along with a @(tsee set-enforce-redundancy) command that precedes them.</p>

   @(def must-be-redundant)"
  (defmacro must-be-redundant
    (&rest forms)
    `(encapsulate nil (set-enforce-redundancy t) ,@FORMS)))