defirrelevant

(in-package "ACL2")

(defmacro+ defirrelevant
  (name &key
    type
    body
    (parents 'nil parents-p)
    short
    (long 'nil long-p))
  :parents (std/util)
  :short "Define an irrelevant value of a type."
  `(define ,NAME
    nil
    :returns (irr ,TYPE)
    ,@(AND PARENTS-P `(:PARENTS ,PARENTS))
    :short ,SHORT
    :long ,(IF LONG-P
     LONG
     (XDOC::TOPSTRING
      (XDOC::P "This can be used as a dummy value of the type.")))
    ,BODY
    ///
    (in-theory (disable (:e ,NAME)))))