		Search-engine friendly clone of the ACL2 documentation.

Wirelist

Wirelist-find

(wirelist-find name x) searches for a name in a wirelist.

Signature
(wirelist-find name x) → wire
Arguments: name — Guard (name-p name).; x — Guard (wirelist-p x).
Returns: wire — Type (iff (wire-p wire) wire).

Definitions and Theorems

Function: wirelist-find

(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: return-type-of-wirelist-find

(defthm return-type-of-wirelist-find
  (b* ((wire (wirelist-find name x)))
    (iff (wire-p wire) wire))
  :rule-classes :rewrite)

Theorem: wirelist-find-of-name-fix-name

(defthm wirelist-find-of-name-fix-name
  (equal (wirelist-find (name-fix name) x)
         (wirelist-find name x)))

Theorem: wirelist-find-name-equiv-congruence-on-name

(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: wirelist-find-of-wirelist-fix-x

(defthm wirelist-find-of-wirelist-fix-x
  (equal (wirelist-find name (wirelist-fix x))
         (wirelist-find name x)))

Theorem: wirelist-find-wirelist-equiv-congruence-on-x

(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)