• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
      • B*
      • Defunc
      • Fty
      • Apt
      • Std/util
        • Defprojection
        • Deflist
        • Defaggregate
        • Define
          • Returns-specifiers
          • Extended-formals
          • Defret
          • Define-guards
          • Defret-mutual
          • Post-define-hook
          • More-returns
          • Raise
          • Defmapping
          • Defenum
          • Add-io-pairs
          • Defalist
          • Defmapappend
          • Returns-specifiers
          • Defarbrec
          • Defines
          • Define-sk
          • Error-value-tuples
          • Defmax-nat
          • Defmin-int
          • Deftutorial
          • Extended-formals
          • Defrule
          • Defval
          • Defsurj
          • Defiso
          • Defconstrained-recognizer
          • Deffixer
          • Defmvtypes
          • Defconsts
          • Defthm-unsigned-byte-p
          • Support
          • Defthm-signed-byte-p
          • Defthm-natp
          • Defund-sk
          • Defmacro+
          • Defsum
          • Defthm-commutative
          • Definj
          • Defirrelevant
          • Defredundant
        • Defdata
        • Defrstobj
        • Seq
        • Match-tree
        • Defrstobj
        • With-supporters
        • Def-partial-measure
        • Template-subst
        • Soft
        • Defthm-domain
        • Event-macros
        • Def-universal-equiv
        • Def-saved-obligs
        • With-supporters-after
        • Definec
        • Sig
        • Outer-local
        • Data-structures
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Support
    • Define
    • Er

    Raise

    Shorthand for causing hard errors.

    (raise &rest args) is equivalent to (er hard? ...), but it automatically fills in the function name using __function__.

    This only works in contexts where __function__ is bound, e.g., the body of a define or within a defconsts form. In these contexts, rather than write something like:

    (er hard? __function__ "bad input value ~x0~%" x)

    You can just write:

    (raise "bad input value ~x0~%" x)

    Logically raise just returns nil.

    Macro: raise

    (defmacro raise (&rest args)
      (cons 'er
            (cons 'hard?
                  (cons '__function__ args))))