Basic constructor macro for lift-info structures.
(make-lift-info [:pred <pred>] [:def <def>] [:hyps <hyps>])
This is the usual way to construct lift-info structures. It simply conses together a structure with the specified fields.
This macro generates a new lift-info structure from scratch. See also change-lift-info, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-lift-info (&rest args) (std::make-aggregate 'lift-info args '((:pred) (:def) (:hyps)) 'make-lift-info nil))
Function:
(defun lift-info (pred def hyps) (declare (xargs :guard (and (symbolp pred) (definitionp def) (true-listp hyps)))) (declare (xargs :guard t)) (let ((__function__ 'lift-info)) (declare (ignorable __function__)) (b* ((pred (mbe :logic (symbol-fix pred) :exec pred)) (def (mbe :logic (definition-fix def) :exec def)) (hyps (mbe :logic (list-fix hyps) :exec hyps))) (list (cons 'pred pred) (cons 'def def) (cons 'hyps hyps)))))