		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-rel-name-set-to-list

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

Signature
(lift-rel-name-set-to-list names wrld) → syms
Arguments: names — Guard (name-setp names).; wrld — Guard (plist-worldp wrld).
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-rel-name-set-to-list

(defun lift-rel-name-set-to-list (names wrld)
  (declare (xargs :guard (and (name-setp names)
                              (plist-worldp wrld))))
  (let ((__function__ 'lift-rel-name-set-to-list))
    (declare (ignorable __function__))
    (cond ((emptyp names) nil)
          (t (cons (lift-rel-name (head names) wrld)
                   (lift-rel-name-set-to-list (tail names)
                                              wrld))))))

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

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