		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-var-name-set-to-list

Lift a set of PFCS variable names to a list of ACL2 symbols.

Signature
(lift-var-name-set-to-list names state) → syms
Arguments: names — Guard (name-setp names).
Returns: syms — Type (symbol-listp syms).

The order of the list is according to the total order that osets are based on.

Definitions and Theorems

Function: lift-var-name-set-to-list

(defun lift-var-name-set-to-list (names state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (name-setp names)))
  (let ((__function__ 'lift-var-name-set-to-list))
    (declare (ignorable __function__))
    (cond ((emptyp names) nil)
          (t (cons (lift-var-name (head names) state)
                   (lift-var-name-set-to-list (tail names)
                                              state))))))

Theorem: symbol-listp-of-lift-var-name-set-to-list

(defthm symbol-listp-of-lift-var-name-set-to-list
  (b* ((syms (lift-var-name-set-to-list names state)))
    (symbol-listp syms))
  :rule-classes :rewrite)