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