		Search-engine friendly clone of the ACL2 documentation.

Vl-make-paramdecloverrides

Vl-find-namedparamvalue

Signature
(vl-find-namedparamvalue name args) → arg
Arguments: name — Guard (stringp name).; args — Guard (vl-namedparamvaluelist-p args).
Returns: arg — Type (equal (vl-namedparamvalue-p arg) (if arg t nil)).

Definitions and Theorems

Function: vl-find-namedparamvalue

(defun vl-find-namedparamvalue (name args)
  (declare (xargs :guard (and (stringp name)
                              (vl-namedparamvaluelist-p args))))
  (let ((__function__ 'vl-find-namedparamvalue))
    (declare (ignorable __function__))
    (b* (((when (atom args)) nil)
         (arg1 (vl-namedparamvalue-fix (car args)))
         ((when (equal (vl-namedparamvalue->name arg1)
                       (string-fix name)))
          arg1))
      (vl-find-namedparamvalue name (cdr args)))))

Theorem: return-type-of-vl-find-namedparamvalue

(defthm return-type-of-vl-find-namedparamvalue
  (b* ((arg (vl-find-namedparamvalue name args)))
    (equal (vl-namedparamvalue-p arg)
           (if arg t nil)))
  :rule-classes :rewrite)

Theorem: vl-find-namedparamvalue-when-member-of-vl-namedparamvaluelist->names

(defthm
 vl-find-namedparamvalue-when-member-of-vl-namedparamvaluelist->names
 (implies (and (member name
                       (vl-namedparamvaluelist->names args))
               (stringp name))
          (vl-find-namedparamvalue name args)))

Theorem: vl-find-namedparamvalue-of-str-fix-name

(defthm vl-find-namedparamvalue-of-str-fix-name
  (equal (vl-find-namedparamvalue (str-fix name)
                                  args)
         (vl-find-namedparamvalue name args)))

Theorem: vl-find-namedparamvalue-streqv-congruence-on-name

(defthm vl-find-namedparamvalue-streqv-congruence-on-name
  (implies (streqv name name-equiv)
           (equal (vl-find-namedparamvalue name args)
                  (vl-find-namedparamvalue name-equiv args)))
  :rule-classes :congruence)

Theorem: vl-find-namedparamvalue-of-vl-namedparamvaluelist-fix-args

(defthm vl-find-namedparamvalue-of-vl-namedparamvaluelist-fix-args
 (equal
    (vl-find-namedparamvalue name (vl-namedparamvaluelist-fix args))
    (vl-find-namedparamvalue name args)))

Theorem: vl-find-namedparamvalue-vl-namedparamvaluelist-equiv-congruence-on-args

(defthm
 vl-find-namedparamvalue-vl-namedparamvaluelist-equiv-congruence-on-args
 (implies (vl-namedparamvaluelist-equiv args args-equiv)
          (equal (vl-find-namedparamvalue name args)
                 (vl-find-namedparamvalue name args-equiv)))
 :rule-classes :congruence)