Recognizer for vl-typedef structures.
(vl-typedef-p x) → *
Function:
(defun vl-typedef-p (x) (declare (xargs :guard t)) (let ((__function__ 'vl-typedef-p)) (declare (ignorable __function__)) (and (consp x) (eq (car x) :vl-typedef) (mbe :logic (and (alistp (cdr x)) (equal (strip-cars (cdr x)) '(name type atts minloc maxloc warnings comments))) :exec (fty::alist-with-carsp (cdr x) '(name type atts minloc maxloc warnings comments))) (b* ((name (cdr (std::da-nth 0 (cdr x)))) (type (cdr (std::da-nth 1 (cdr x)))) (atts (cdr (std::da-nth 2 (cdr x)))) (minloc (cdr (std::da-nth 3 (cdr x)))) (maxloc (cdr (std::da-nth 4 (cdr x)))) (warnings (cdr (std::da-nth 5 (cdr x)))) (comments (cdr (std::da-nth 6 (cdr x))))) (and (stringp name) (vl-datatype-p type) (vl-atts-p atts) (vl-location-p minloc) (vl-location-p maxloc) (vl-warninglist-p warnings) (vl-commentmap-p comments))))))
Theorem:
(defthm consp-when-vl-typedef-p (implies (vl-typedef-p x) (consp x)) :rule-classes :compound-recognizer)