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