		Search-engine friendly clone of the ACL2 documentation.

Vl-funtemplate-p

Vl-find-funtemplate

Find a function template by name.

Signature
(vl-find-funtemplate name templates) → template?
Arguments: name — Guard (stringp name).; templates — Guard (vl-funtemplatelist-p templates).
Returns: template? — Type (equal (vl-funtemplate-p template?) (if template? t nil)), given the guard.

Definitions and Theorems

Function: vl-find-funtemplate

(defun vl-find-funtemplate (name templates)
  (declare (xargs :guard (and (stringp name)
                              (vl-funtemplatelist-p templates))))
  (let ((__function__ 'vl-find-funtemplate))
    (declare (ignorable __function__))
    (cond ((atom templates) nil)
          ((equal name
                  (vl-funtemplate->name (car templates)))
           (car templates))
          (t (vl-find-funtemplate name (cdr templates))))))

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

(defthm return-type-of-vl-find-funtemplate
  (implies (and (force (stringp name))
                (force (vl-funtemplatelist-p templates)))
           (b* ((template? (vl-find-funtemplate name templates)))
             (equal (vl-funtemplate-p template?)
                    (if template? t nil))))
  :rule-classes :rewrite)