		Search-engine friendly clone of the ACL2 documentation.

Defequal-table

Defequal-trim-call-args

Signature
(defequal-trim-call-args args) → trimmed-args
Arguments: args — Guard (true-listp args).
Returns: trimmed-args — Type (true-listp trimmed-args).

Definitions and Theorems

Function: defequal-trim-call-args

(defun defequal-trim-call-args (args)
  (declare (xargs :guard (true-listp args)))
  (let ((__function__ 'defequal-trim-call-args))
    (declare (ignorable __function__))
    (cond ((endp args) nil)
          ((member-eq (car args)
                      '(:print :show-only))
           (defequal-trim-call-args (cddr args)))
          (t (cons (car args)
                   (defequal-trim-call-args (cdr args)))))))

Theorem: true-listp-of-defequal-trim-call-args

(defthm true-listp-of-defequal-trim-call-args
  (b* ((trimmed-args (defequal-trim-call-args args)))
    (true-listp trimmed-args))
  :rule-classes :rewrite)