An irrelevant type qualifier.
(irr-type-qual) → acl2::irr
This can be used as a dummy value of the type.
Function:
(defun irr-type-qual nil (declare (xargs :guard t)) (let ((__function__ 'irr-type-qual)) (declare (ignorable __function__)) (type-qual-const)))
Theorem:
(defthm type-qualp-of-irr-type-qual (b* ((acl2::irr (irr-type-qual))) (type-qualp acl2::irr)) :rule-classes :rewrite)