Recognizer for vl-fwdtypedef structures.
(vl-fwdtypedef-p x) → *
Function:
(defun vl-fwdtypedef-p (x) (declare (xargs :guard t)) (let ((__function__ 'vl-fwdtypedef-p)) (declare (ignorable __function__)) (and (consp x) (eq (car x) :vl-fwdtypedef) (mbe :logic (and (alistp (cdr x)) (equal (strip-cars (cdr x)) '(atts kind name loc))) :exec (fty::alist-with-carsp (cdr x) '(atts kind name loc))) (b* ((atts (cdr (std::da-nth 0 (cdr x)))) (kind (cdr (std::da-nth 1 (cdr x)))) (name (cdr (std::da-nth 2 (cdr x)))) (loc (cdr (std::da-nth 3 (cdr x))))) (and (vl-atts-p atts) (vl-fwdtypedefkind-p kind) (stringp name) (vl-location-p loc))))))
Theorem:
(defthm consp-when-vl-fwdtypedef-p (implies (vl-fwdtypedef-p x) (consp x)) :rule-classes :compound-recognizer)