		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Get-function-header-in-list

Find the function header with a given name in a list of function headers.

Signature
(get-function-header-in-list name headers) → funhead?
Arguments: name — Guard (identifierp name).; headers — Guard (function-header-listp headers).
Returns: funhead? — Type (maybe-function-headerp funhead?).

Definitions and Theorems

Function: get-function-header-in-list

(defun get-function-header-in-list (name headers)
 (declare (xargs :guard (and (identifierp name)
                             (function-header-listp headers))))
 (let ((__function__ 'get-function-header-in-list))
  (declare (ignorable __function__))
  (cond
     ((endp headers) nil)
     (t (if (identifier-equiv name
                              (function-header->name (car headers)))
            (function-header-fix (car headers))
          (get-function-header-in-list name (cdr headers)))))))

Theorem: maybe-function-headerp-of-get-function-header-in-list

(defthm maybe-function-headerp-of-get-function-header-in-list
  (b* ((funhead? (get-function-header-in-list name headers)))
    (maybe-function-headerp funhead?))
  :rule-classes :rewrite)

Theorem: get-function-header-in-list-of-identifier-fix-name

(defthm get-function-header-in-list-of-identifier-fix-name
  (equal (get-function-header-in-list (identifier-fix name)
                                      headers)
         (get-function-header-in-list name headers)))

Theorem: get-function-header-in-list-identifier-equiv-congruence-on-name

(defthm
    get-function-header-in-list-identifier-equiv-congruence-on-name
  (implies (identifier-equiv name name-equiv)
           (equal (get-function-header-in-list name headers)
                  (get-function-header-in-list name-equiv headers)))
  :rule-classes :congruence)

Theorem: get-function-header-in-list-of-function-header-list-fix-headers

(defthm
    get-function-header-in-list-of-function-header-list-fix-headers
  (equal (get-function-header-in-list
              name (function-header-list-fix headers))
         (get-function-header-in-list name headers)))

Theorem: get-function-header-in-list-function-header-list-equiv-congruence-on-headers

(defthm
 get-function-header-in-list-function-header-list-equiv-congruence-on-headers
 (implies (function-header-list-equiv headers headers-equiv)
          (equal (get-function-header-in-list name headers)
                 (get-function-header-in-list name headers-equiv)))
 :rule-classes :congruence)