		Search-engine friendly clone of the ACL2 documentation.

Defmapping-event-generation

Defmapping-gen-var-aa/bb

Generate the list of variables (aa1 ... aan) or (bb1 ... bbm) described in the documentation.

Signature
(defmapping-gen-var-aa/bb a1/b1...an/bm) → aa1/bb1...aan/bbm
Arguments: a1/b1...an/bm — Guard (symbol-listp a1/b1...an/bm).
Returns: aa1/bb1...aan/bbm — A symbol-listp.

We generate these by appending $ to each of (a1 ... an) or (b1 ... bm), using genvar to ensure that we do not introduce clashes.

Definitions and Theorems

Function: defmapping-gen-var-aa/bb

(defun defmapping-gen-var-aa/bb (a1/b1...an/bm)
 (declare (xargs :guard (symbol-listp a1/b1...an/bm)))
 (let ((__function__ 'defmapping-gen-var-aa/bb))
  (declare (ignorable __function__))
  (cond
   ((endp a1/b1...an/bm) nil)
   (t
     (b*
       ((aa2/bb2...aan/bbm
             (defmapping-gen-var-aa/bb (cdr a1/b1...an/bm)))
        (a1/b1 (car a1/b1...an/bm))
        (aa1/bb1 (genvar a1/b1 (str::cat (symbol-name a1/b1) "$")
                         nil
                         (append a1/b1...an/bm aa2/bb2...aan/bbm))))
       (cons aa1/bb1 aa2/bb2...aan/bbm))))))