		Search-engine friendly clone of the ACL2 documentation.

Defmapping-event-generation

Defmapping-gen-var-b1...bm

Generate the list of variables (b1 ... bm) described in the documentation.

Signature
(defmapping-gen-var-b1...bm beta$ wrld) → b1...bm
Arguments: beta$ — Guard (pseudo-termfnp beta$).; wrld — Guard (plist-worldp wrld).
Returns: b1...bm — A symbol-listp.

We use the formal parameters of the conversion \beta.

Definitions and Theorems

Function: defmapping-gen-var-b1...bm

(defun defmapping-gen-var-b1...bm (beta$ wrld)
  (declare (xargs :guard (and (pseudo-termfnp beta$)
                              (plist-worldp wrld))))
  (let ((__function__ 'defmapping-gen-var-b1...bm))
    (declare (ignorable __function__))
    (cond ((symbolp beta$) (formals beta$ wrld))
          (t (lambda-formals beta$)))))