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