Find the function header with a given name in a list of function headers.
(get-function-header-in-list name headers) → funhead?
Function:
(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:
(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:
(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:
(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:
(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:
(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)