		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-table-add

Event to update the table of lifted PFCSes.

Signature
(lift-table-add pred def hyps) → even
Arguments: pred — Guard (symbolp pred).; def — Guard (definitionp def).; hyps — Guard (true-listp hyps).
Returns: even — Type (pseudo-event-formp even).

This adds an entry to the table for the definition passed as argument.

Definitions and Theorems

Function: lift-table-add

(defun lift-table-add (pred def hyps)
  (declare (xargs :guard (and (symbolp pred)
                              (definitionp def)
                              (true-listp hyps))))
  (let ((__function__ 'lift-table-add))
    (declare (ignorable __function__))
    (b* ((name (definition->name def))
         (info (make-lift-info :pred pred
                               :def def
                               :hyps hyps)))
      (cons 'table
            (cons 'lift-table
                  (cons name
                        (cons (cons 'quote (cons info 'nil))
                              'nil)))))))

Theorem: pseudo-event-formp-of-lift-table-add

(defthm pseudo-event-formp-of-lift-table-add
  (b* ((even (lift-table-add pred def hyps)))
    (pseudo-event-formp even))
  :rule-classes :rewrite)