		Search-engine friendly clone of the ACL2 documentation.

Std/util

Defirrelevant

Define an irrelevant value of a type.

Macro: defirrelevant

(defmacro defirrelevant
          (name &key type body (parents 'nil parents-p)
                short)
 (cons
  'define
  (cons
   name
   (cons
    'nil
    (cons
     ':returns
     (cons
      (cons 'irr (cons type 'nil))
      (append
       (and parents-p
            (cons ':parents (cons parents '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))))))))))))))