		Search-engine friendly clone of the ACL2 documentation.

Esim-vl-find-io

Esim-vl-find-io-main

(esim-vl-find-io-main basename x) finds the first iopattern entry in x with this basename.

Definitions and Theorems

Function: esim-vl-find-io-main

(defun esim-vl-find-io-main (basename x)
  (declare (xargs :guard (and (stringp basename)
                              (esim-vl-iopattern-entrylist-p x))))
  (cond ((atom x) nil)
        ((equal (esim-vl-iopattern-entry->basename (car x))
                basename)
         (llist-fix (car x)))
        (t (esim-vl-find-io-main basename (cdr x)))))

Theorem: vl-emodwirelist-p-of-esim-vl-find-io-main

(defthm vl-emodwirelist-p-of-esim-vl-find-io-main
  (implies (esim-vl-iopattern-entrylist-p x)
           (vl-emodwirelist-p (esim-vl-find-io-main basename x))))

Theorem: true-listp-of-esim-vl-find-io-main

(defthm true-listp-of-esim-vl-find-io-main
  (true-listp (esim-vl-find-io-main basename x))
  :rule-classes :type-prescription)