(wirelist-find name x) searches for a name in a wirelist.
(wirelist-find name x) → wire
Function:
(defun wirelist-find (name x) (declare (xargs :guard (and (name-p name) (wirelist-p x)))) (let ((__function__ 'wirelist-find)) (declare (ignorable __function__)) (cond ((atom x) nil) ((equal (wire->name (car x)) (name-fix name)) (wire-fix (car x))) (t (wirelist-find name (cdr x))))))
Theorem:
(defthm return-type-of-wirelist-find (b* ((wire (wirelist-find name x))) (iff (wire-p wire) wire)) :rule-classes :rewrite)
Theorem:
(defthm wirelist-find-of-name-fix-name (equal (wirelist-find (name-fix name) x) (wirelist-find name x)))
Theorem:
(defthm wirelist-find-name-equiv-congruence-on-name (implies (name-equiv name name-equiv) (equal (wirelist-find name x) (wirelist-find name-equiv x))) :rule-classes :congruence)
Theorem:
(defthm wirelist-find-of-wirelist-fix-x (equal (wirelist-find name (wirelist-fix x)) (wirelist-find name x)))
Theorem:
(defthm wirelist-find-wirelist-equiv-congruence-on-x (implies (wirelist-equiv x x-equiv) (equal (wirelist-find name x) (wirelist-find name x-equiv))) :rule-classes :congruence)