		Search-engine friendly clone of the ACL2 documentation.

Rewrite

Make-rewrite

Basic constructor macro for rewrite structures.

Syntax

(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.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-rewrite

(defmacro make-rewrite (&rest args)
  (std::make-aggregate 'rewrite
                       args '((:hyps) (:equiv) (:lhs) (:rhs))
                       'make-rewrite
                       nil))

Function: rewrite

(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))))