		Search-engine friendly clone of the ACL2 documentation.

Ihs-utilities

Definition-free-theory

Returns the theory with all :DEFINITION rules deleted.

Definitions and Theorems

Function: definition-free-theory-rec

(defun definition-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) :definition))
         (definition-free-theory-rec (cdr theory)
                                     ans))
        (t (definition-free-theory-rec (cdr theory)
                                       (cons (car theory) ans)))))

Function: definition-free-theory

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