• 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
        • Must-fail-with-soft-error
        • Must-fail-with-hard-error
        • Must-fail-with-error
        • Must-fail-local
      • 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-fail

Must-fail-local

A local variant of must-fail.

This is useful to overcome the problem discussed in the caveat in the documentation of must-fail.

Macro: must-fail-local

(defmacro must-fail-local (&rest args)
  (cons 'local
        (cons (cons 'must-fail args) 'nil)))