		Search-engine friendly clone of the ACL2 documentation.

Deftrans

Deftrans-parse-keywords

Signature
(deftrans-parse-keywords list) → (mv extra-args with-output-off bodies)
Arguments: list — Guard (true-listp list).
Returns: extra-args — Type (true-listp extra-args).; bodies — Type (alistp bodies).

Definitions and Theorems

Function: deftrans-parse-keywords

(defun deftrans-parse-keywords (list)
 (declare (xargs :guard (true-listp list)))
 (let ((__function__ 'deftrans-parse-keywords))
  (declare (ignorable __function__))
  (b*
   ((pairs (take-pairs list))
    (extra-args (b* ((lookup (assoc-eq :extra-args pairs)))
                  (if (and lookup (true-listp (cdr lookup)))
                      (cdr lookup)
                    nil)))
    (with-output-off
         (b* ((lookup (assoc-eq :with-output-off pairs)))
           (if lookup (cdr lookup)
             '(:other-than summary error))))
    (bodies
        (remove-assoc-eq
             :extra-args (remove-assoc-eq :with-output-off pairs))))
   (mv extra-args with-output-off bodies))))

Theorem: true-listp-of-deftrans-parse-keywords.extra-args

(defthm true-listp-of-deftrans-parse-keywords.extra-args
  (b* (((mv ?extra-args ?with-output-off ?bodies)
        (deftrans-parse-keywords list)))
    (true-listp extra-args))
  :rule-classes :rewrite)

Theorem: alistp-of-deftrans-parse-keywords.bodies

(defthm alistp-of-deftrans-parse-keywords.bodies
  (b* (((mv ?extra-args ?with-output-off ?bodies)
        (deftrans-parse-keywords list)))
    (alistp bodies))
  :rule-classes :rewrite)