Event to update the table of lifted PFCSes.
(lift-table-add pred def hyps) → even
This adds an entry to the table for the definition passed as argument.
Function:
(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:
(defthm pseudo-event-formp-of-lift-table-add (b* ((even (lift-table-add pred def hyps))) (pseudo-event-formp even)) :rule-classes :rewrite)