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