		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Get-function-definition-in-function-definitions

Find the definition of a function with a given name in a list of function definitions.

Signature
(get-function-definition-in-function-definitions name fundefs) → fundef?
Arguments: name — Guard (identifierp name).; fundefs — Guard (function-definition-listp fundefs).
Returns: fundef? — Type (maybe-function-definitionp fundef?).

This is used when looking up a function definition in a function recursion.

We return nil if the function definition is not found.

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.

Definitions and Theorems

Function: get-function-definition-in-function-definitions

(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: maybe-function-definitionp-of-get-function-definition-in-function-definitions

(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: get-function-definition-in-function-definitions-of-identifier-fix-name

(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: get-function-definition-in-function-definitions-identifier-equiv-congruence-on-name

(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: get-function-definition-in-function-definitions-of-function-definition-list-fix-fundefs

(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: get-function-definition-in-function-definitions-function-definition-list-equiv-congruence-on-fundefs

(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)