		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-table-add

Event to update the table of lifted PFCSes.

Signature
(lift-table-add def hyps) → even
Arguments: 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 (def hyps)
  (declare (xargs :guard (and (definitionp def)
                              (true-listp hyps))))
  (let ((__function__ 'lift-table-add))
    (declare (ignorable __function__))
    (b* ((info (make-lift-info :def def :hyps hyps)))
      (cons 'table
            (cons 'lift-table
                  (cons (definition->name def)
                        (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 def hyps)))
    (pseudo-event-formp even))
  :rule-classes :rewrite)