		Search-engine friendly clone of the ACL2 documentation.

Atj-deep-code-generation

Atj-gen-deep-fndef-methods

Lift atj-gen-deep-fndef-method to lists.

Signature
(atj-gen-deep-fndef-methods fns guards$ verbose$ wrld) → methods
Arguments: fns — Guard (symbol-listp fns).; guards$ — Guard (booleanp guards$).; verbose$ — Guard (booleanp verbose$).; wrld — Guard (plist-worldp wrld).
Returns: methods — Type (jmethod-listp methods).

Definitions and Theorems

Function: atj-gen-deep-fndef-methods

(defun atj-gen-deep-fndef-methods (fns guards$ verbose$ wrld)
  (declare (xargs :guard (and (symbol-listp fns)
                              (booleanp guards$)
                              (booleanp verbose$)
                              (plist-worldp wrld))))
  (let ((__function__ 'atj-gen-deep-fndef-methods))
    (declare (ignorable __function__))
    (if (endp fns)
        nil
      (b* ((first-method
                (atj-gen-deep-fndef-method (car fns)
                                           guards$ verbose$ wrld))
           (rest-methods
                (atj-gen-deep-fndef-methods (cdr fns)
                                            guards$ verbose$ wrld)))
        (cons first-method rest-methods)))))

Theorem: jmethod-listp-of-atj-gen-deep-fndef-methods

(defthm jmethod-listp-of-atj-gen-deep-fndef-methods
 (b*
  ((methods (atj-gen-deep-fndef-methods fns guards$ verbose$ wrld)))
  (jmethod-listp methods))
 :rule-classes :rewrite)