		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

Lookup-transform-argument

Signature
(lookup-transform-argument args arg-name) → *
Arguments: args — Guard (transform-argument-listp args).; arg-name — Guard (stringp arg-name).

Definitions and Theorems

Function: lookup-transform-argument

(defun lookup-transform-argument (args arg-name)
 (declare (xargs :guard (and (transform-argument-listp args)
                             (stringp arg-name))))
 (let ((__function__ 'lookup-transform-argument))
  (declare (ignorable __function__))
  (if (endp args)
      nil
   (b* (((transform-argument arg) (car args)))
    (if
     (equal arg-name (identifier->name arg.name))
     (let ((arg-val arg.value))
       (transform-argument-value-case arg-val
                                      :identifier arg-val.name
                                      :identifier-list arg-val.names
                                      :term arg-val.get
                                      :bool arg-val.val))
     (lookup-transform-argument (cdr args)
                                arg-name))))))