		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-symbols

Lift atj-gen-symbol to lists.

Signature
(atj-gen-symbols symbols deep$ guards$) → exprs
Arguments: symbols — Guard (symbol-listp symbols).; deep$ — Guard (symbolp deep$).; guards$ — Guard (symbolp guards$).
Returns: exprs — Type (jexpr-listp exprs).

Definitions and Theorems

Function: atj-gen-symbols

(defun atj-gen-symbols (symbols deep$ guards$)
  (declare (xargs :guard (and (symbol-listp symbols)
                              (symbolp deep$)
                              (symbolp guards$))))
  (let ((__function__ 'atj-gen-symbols))
    (declare (ignorable __function__))
    (cond ((endp symbols) nil)
          (t (cons (atj-gen-symbol (car symbols)
                                   deep$ guards$)
                   (atj-gen-symbols (cdr symbols)
                                    deep$ guards$))))))

Theorem: jexpr-listp-of-atj-gen-symbols

(defthm jexpr-listp-of-atj-gen-symbols
  (b* ((exprs (atj-gen-symbols symbols deep$ guards$)))
    (jexpr-listp exprs))
  :rule-classes :rewrite)