• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
      • Cgen
      • Run-script
      • Std/testing
        • Must-fail
        • Assert!-stobj
        • Must-eval-to
        • Assert!
        • Must-succeed
        • Must-succeed*
        • Assert?
        • Must-fail-with-soft-error
        • Must-fail-with-hard-error
        • Must-fail-with-error
        • Must-eval-to-t
        • Must-prove
        • Must-not-prove
        • Must-not-be-table-key
        • Must-be-redundant
          • Must-fail-local
          • Must-be-table-key
          • Assert-equal
    • Std/testing
    • Errors

    Must-be-redundant

    A top-level assert$-like command to ensure that given forms are redundant.

    The forms are put into an encapsulate, along with a set-enforce-redundancy command that precedes them.

    Macro: must-be-redundant

    (defmacro must-be-redundant (&rest forms)
      (cons 'encapsulate
            (cons 'nil
                  (cons '(set-enforce-redundancy t)
                        forms))))