		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-thm-called-lift-thms

List of lifting theorems for a set of relations.

Signature
(lift-thm-called-lift-thms rels) → called-lift-thms
Arguments: rels — Guard (symbol-listp rels).

These are used as rewrite rules in the caller's lifting theorem.

Definitions and Theorems

Function: lift-thm-called-lift-thms

(defun lift-thm-called-lift-thms (rels)
  (declare (xargs :guard (symbol-listp rels)))
  (let ((__function__ 'lift-thm-called-lift-thms))
    (declare (ignorable __function__))
    (b* (((when (endp rels)) nil)
         (rel (car rels)))
      (cons (acl2::packn-pos (list 'definition-satp-of-
                                   rel '-to-shallow)
                             rel)
            (lift-thm-called-lift-thms (cdr rels))))))