		Search-engine friendly clone of the ACL2 documentation.

Ihs-utilities

Rewrite-free-theory

Returns the theory with all :REWRITE rules deleted.

Definitions and Theorems

Function: rewrite-free-theory-rec

(defun rewrite-free-theory-rec (theory ans)
  (declare (xargs :guard (and (true-listp theory)
                              (true-listp ans))))
  (cond ((endp theory) (reverse ans))
        ((and (consp (car theory))
              (equal (caar theory) :rewrite))
         (rewrite-free-theory-rec (cdr theory)
                                  ans))
        (t (rewrite-free-theory-rec (cdr theory)
                                    (cons (car theory) ans)))))

Function: rewrite-free-theory

(defun rewrite-free-theory (theory)
  (declare (xargs :guard (true-listp theory)))
  (rewrite-free-theory-rec theory nil))