		Search-engine friendly clone of the ACL2 documentation.

Program-execution

Lookup-funarg

Look up a function argument with a given name in a list of function arguments.

Signature
(lookup-funarg name args) → arg
Arguments: name — Guard (identifierp name).; args — Guard (funarg-listp args).
Returns: arg — Type (funarg-optionp arg).

Return the first match, if any. Return nil if there is no match.

Definitions and Theorems

Function: lookup-funarg

(defun lookup-funarg (name args)
  (declare (xargs :guard (and (identifierp name)
                              (funarg-listp args))))
  (let ((__function__ 'lookup-funarg))
    (declare (ignorable __function__))
    (b* (((when (endp args)) nil)
         (arg (car args))
         ((when (identifier-equiv name (funarg->name arg)))
          (funarg-fix arg)))
      (lookup-funarg name (cdr args)))))

Theorem: funarg-optionp-of-lookup-funarg

(defthm funarg-optionp-of-lookup-funarg
  (b* ((arg (lookup-funarg name args)))
    (funarg-optionp arg))
  :rule-classes :rewrite)

Theorem: lookup-funarg-of-identifier-fix-name

(defthm lookup-funarg-of-identifier-fix-name
  (equal (lookup-funarg (identifier-fix name)
                        args)
         (lookup-funarg name args)))

Theorem: lookup-funarg-identifier-equiv-congruence-on-name

(defthm lookup-funarg-identifier-equiv-congruence-on-name
  (implies (identifier-equiv name name-equiv)
           (equal (lookup-funarg name args)
                  (lookup-funarg name-equiv args)))
  :rule-classes :congruence)

Theorem: lookup-funarg-of-funarg-list-fix-args

(defthm lookup-funarg-of-funarg-list-fix-args
  (equal (lookup-funarg name (funarg-list-fix args))
         (lookup-funarg name args)))

Theorem: lookup-funarg-funarg-list-equiv-congruence-on-args

(defthm lookup-funarg-funarg-list-equiv-congruence-on-args
  (implies (funarg-list-equiv args args-equiv)
           (equal (lookup-funarg name args)
                  (lookup-funarg name args-equiv)))
  :rule-classes :congruence)