		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)