An irrelevant declaration specifier.
(irr-declspec) → acl2::irr
This can be used as a dummy value of the type.
Function:
(defun irr-declspec nil (declare (xargs :guard t)) (let ((__function__ 'irr-declspec)) (declare (ignorable __function__)) (declspec-tyspec (irr-type-spec))))
Theorem:
(defthm declspecp-of-irr-declspec (b* ((acl2::irr (irr-declspec))) (declspecp acl2::irr)) :rule-classes :rewrite)