Recognizer for decl structures.
(declp x) → *
Function:
(defun declp (x) (declare (xargs :guard t)) (let ((__function__ 'declp)) (declare (ignorable __function__)) (and (consp x) (cond ((or (atom x) (eq (car x) :decl)) (and (true-listp (cdr x)) (eql (len (cdr x)) 5) (b* ((extension (std::da-nth 0 (cdr x))) (specs (std::da-nth 1 (cdr x))) (init (std::da-nth 2 (cdr x))) (asm? (std::da-nth 3 (cdr x))) (attrib (std::da-nth 4 (cdr x)))) (and (booleanp extension) (declspec-listp specs) (initdeclor-listp init) (asm-name-spec-optionp asm?) (attrib-spec-listp attrib))))) (t (and (eq (car x) :statassert) (and (true-listp (cdr x)) (eql (len (cdr x)) 1)) (b* ((unwrap (std::da-nth 0 (cdr x)))) (statassertp unwrap))))))))
Theorem:
(defthm consp-when-declp (implies (declp x) (consp x)) :rule-classes :compound-recognizer)