Find the definition of a function with a given name in a list of function definitions.
(get-function-definition-in-function-definitions name fundefs) → fundef?
This is used when looking up a function definition in a function recursion.
We return
We look up the definitions in order. In well-formed lists of function definitions, the function names are unique, so any order would yield the same result.
Function:
(defun get-function-definition-in-function-definitions (name fundefs) (declare (xargs :guard (and (identifierp name) (function-definition-listp fundefs)))) (let ((__function__ 'get-function-definition-in-function-definitions)) (declare (ignorable __function__)) (b* (((when (endp fundefs)) nil) ((when (identifier-equiv name (function-header->name (function-definition->header (car fundefs))))) (function-definition-fix (car fundefs)))) (get-function-definition-in-function-definitions name (cdr fundefs)))))
Theorem:
(defthm maybe-function-definitionp-of-get-function-definition-in-function-definitions (b* ((fundef? (get-function-definition-in-function-definitions name fundefs))) (maybe-function-definitionp fundef?)) :rule-classes :rewrite)
Theorem:
(defthm get-function-definition-in-function-definitions-of-identifier-fix-name (equal (get-function-definition-in-function-definitions (identifier-fix name) fundefs) (get-function-definition-in-function-definitions name fundefs)))
Theorem:
(defthm get-function-definition-in-function-definitions-identifier-equiv-congruence-on-name (implies (identifier-equiv name name-equiv) (equal (get-function-definition-in-function-definitions name fundefs) (get-function-definition-in-function-definitions name-equiv fundefs))) :rule-classes :congruence)
Theorem:
(defthm get-function-definition-in-function-definitions-of-function-definition-list-fix-fundefs (equal (get-function-definition-in-function-definitions name (function-definition-list-fix fundefs)) (get-function-definition-in-function-definitions name fundefs)))
Theorem:
(defthm get-function-definition-in-function-definitions-function-definition-list-equiv-congruence-on-fundefs (implies (function-definition-list-equiv fundefs fundefs-equiv) (equal (get-function-definition-in-function-definitions name fundefs) (get-function-definition-in-function-definitions name fundefs-equiv))) :rule-classes :congruence)