An irrelevant structure/union/enumeration declaration.
(irr-tag-declon) → acl2::irr
This can be used as a dummy value of the type.
Function:
(defun irr-tag-declon nil (declare (xargs :guard t)) (let ((__function__ 'irr-tag-declon)) (declare (ignorable __function__)) (make-tag-declon-struct :tag (irr-ident) :members nil)))
Theorem:
(defthm tag-declonp-of-irr-tag-declon (b* ((acl2::irr (irr-tag-declon))) (tag-declonp acl2::irr)) :rule-classes :rewrite)