An irrelevant possibly ambiguous declaration or statement.
(irr-amb?-decl/stmt) → acl2::irr
This can be used as a dummy value of the type.
Function:
(defun irr-amb?-decl/stmt nil (declare (xargs :guard t)) (let ((__function__ 'irr-amb?-decl/stmt)) (declare (ignorable __function__)) (amb?-decl/stmt-stmt (irr-expr))))
Theorem:
(defthm amb?-decl/stmt-p-of-irr-amb?-decl/stmt (b* ((acl2::irr (irr-amb?-decl/stmt))) (amb?-decl/stmt-p acl2::irr)) :rule-classes :rewrite)