An irrelevant assembler name specifier.
(irr-asm-name-spec) → acl2::irr
This can be used as a dummy value of the type.
Function:
(defun irr-asm-name-spec nil (declare (xargs :guard t)) (let ((__function__ 'irr-asm-name-spec)) (declare (ignorable __function__)) (asm-name-spec nil (keyword-uscores-none))))
Theorem:
(defthm asm-name-specp-of-irr-asm-name-spec (b* ((acl2::irr (irr-asm-name-spec))) (asm-name-specp acl2::irr)) :rule-classes :rewrite)