		Search-engine friendly clone of the ACL2 documentation.

Defirrelevant

Define an irrelevant value of a type.

Macro: defirrelevant

(defmacro
 defirrelevant
 (name &key type body short)
 (cons
  'define
  (cons
   name
   (cons
    'nil
    (cons
     ':returns
     (cons
      (cons 'irr (cons type 'nil))
      (cons
       ':short
       (cons
        short
        (cons
         ':long
         (cons
          '(xdoc::topstring
             (xdoc::p
                  "This can be used as a dummy value of the type."))
          (cons
           body
           (cons
            '///
            (cons
             (cons
                'in-theory
                (cons (cons 'disable
                            (cons (cons ':e (cons name 'nil)) 'nil))
                      'nil))
             'nil)))))))))))))