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