		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Lookup-definition

Look up a definition in a list of definitions.

Signature
(lookup-definition name defs) → def?
Arguments: name — Guard (stringp name).; defs — Guard (definition-listp defs).
Returns: def? — Type (definition-optionp def?).

If the list has a definition for the given name, return that definition. Otherwise return nil.

We return the first definition found for that name. In a well-formed lists of definitions, there is at most a definition for each name, and thus the first one found (if any) is also the only one.

Definitions and Theorems

Function: lookup-definition

(defun lookup-definition (name defs)
  (declare (xargs :guard (and (stringp name)
                              (definition-listp defs))))
  (let ((__function__ 'lookup-definition))
    (declare (ignorable __function__))
    (b* (((when (endp defs)) nil)
         (def (car defs))
         ((when (equal (definition->name def)
                       (str-fix name)))
          (definition-fix def)))
      (lookup-definition name (cdr defs)))))

Theorem: definition-optionp-of-lookup-definition

(defthm definition-optionp-of-lookup-definition
  (b* ((def? (lookup-definition name defs)))
    (definition-optionp def?))
  :rule-classes :rewrite)

Theorem: lookup-definition-of-str-fix-name

(defthm lookup-definition-of-str-fix-name
  (equal (lookup-definition (str-fix name) defs)
         (lookup-definition name defs)))

Theorem: lookup-definition-streqv-congruence-on-name

(defthm lookup-definition-streqv-congruence-on-name
  (implies (acl2::streqv name name-equiv)
           (equal (lookup-definition name defs)
                  (lookup-definition name-equiv defs)))
  :rule-classes :congruence)

Theorem: lookup-definition-of-definition-list-fix-defs

(defthm lookup-definition-of-definition-list-fix-defs
  (equal (lookup-definition name (definition-list-fix defs))
         (lookup-definition name defs)))

Theorem: lookup-definition-definition-list-equiv-congruence-on-defs

(defthm lookup-definition-definition-list-equiv-congruence-on-defs
  (implies (definition-list-equiv defs defs-equiv)
           (equal (lookup-definition name defs)
                  (lookup-definition name defs-equiv)))
  :rule-classes :congruence)