Recognizer for wire structures.
(wire-p x) → *
Function:
(defun wire-p (x) (declare (xargs :guard t)) (let ((__function__ 'wire-p)) (declare (ignorable __function__)) (and (std::prod-consp x) (std::prod-consp (std::prod-car x)) (std::prod-consp (std::prod-cdr (std::prod-car x))) (std::prod-consp (std::prod-cdr x)) (std::prod-consp (std::prod-car (std::prod-cdr x))) (std::prod-consp (std::prod-cdr (std::prod-cdr x))) (b* ((name (std::prod-car (std::prod-car x))) (width (std::prod-car (std::prod-cdr (std::prod-car x)))) (low-idx (std::prod-cdr (std::prod-cdr (std::prod-car x)))) (delay (std::prod-car (std::prod-car (std::prod-cdr x)))) (?revp (std::prod-cdr (std::prod-car (std::prod-cdr x)))) (type (std::prod-car (std::prod-cdr (std::prod-cdr x)))) (atts (std::prod-cdr (std::prod-cdr (std::prod-cdr x))))) (and (name-p name) (posp width) (integerp low-idx) (maybe-posp delay) (wiretype type) (attributes-p atts))))))
Theorem:
(defthm consp-when-wire-p (implies (wire-p x) (consp x)) :rule-classes :compound-recognizer)