Basic constructor macro for rewrite structures.
(make-rewrite [:hyps <hyps>] [:equiv <equiv>] [:lhs <lhs>] [:rhs <rhs>])
This is the usual way to construct rewrite structures. It simply conses together a structure with the specified fields.
This macro generates a new rewrite structure from scratch. See also change-rewrite, which can "change" an existing structure, instead.
This is an ordinary
(defmacro make-rewrite (&rest args) (std::make-aggregate 'rewrite args '((:hyps) (:equiv) (:lhs) (:rhs)) 'make-rewrite nil))
(defun rewrite (hyps equiv lhs rhs) (declare (xargs :guard (and (pseudo-term-listp hyps) (pseudo-fnsym-p equiv) (pseudo-termp lhs) (pseudo-termp rhs)))) (declare (xargs :guard t)) (let ((__function__ 'rewrite)) (declare (ignorable __function__)) (b* ((hyps (mbe :logic (pseudo-term-list-fix hyps) :exec hyps)) (equiv (mbe :logic (pseudo-fnsym-fix equiv) :exec equiv)) (lhs (mbe :logic (pseudo-term-fix lhs) :exec lhs)) (rhs (mbe :logic (pseudo-term-fix rhs) :exec rhs))) (list hyps equiv lhs rhs))))