		Search-engine friendly clone of the ACL2 documentation.

Transform-argument-value

Transform-argument-valuep

Recognizer for transform-argument-value structures.

Signature
(transform-argument-valuep x) → *

Definitions and Theorems

Function: transform-argument-valuep

(defun transform-argument-valuep (x)
  (declare (xargs :guard t))
  (let ((__function__ 'transform-argument-valuep))
    (declare (ignorable __function__))
    (and (consp x)
         (cond ((or (atom x) (eq (car x) :identifier))
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 1)
                     (b* ((name (std::da-nth 0 (cdr x))))
                       (identifierp name))))
               ((eq (car x) :identifier-list)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 1)
                     (b* ((names (std::da-nth 0 (cdr x))))
                       (identifier-listp names))))
               ((eq (car x) :term)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 1)
                     (b* ((get (std::da-nth 0 (cdr x))))
                       (expressionp get))))
               (t (and (eq (car x) :bool)
                       (and (true-listp (cdr x))
                            (eql (len (cdr x)) 1))
                       (b* ((val (std::da-nth 0 (cdr x))))
                         (booleanp val))))))))

Theorem: consp-when-transform-argument-valuep

(defthm consp-when-transform-argument-valuep
  (implies (transform-argument-valuep x)
           (consp x))
  :rule-classes :compound-recognizer)