		Search-engine friendly clone of the ACL2 documentation.

Ihs-utilities

Definition-theory

Collects all of the :DEFINITION runes from theory.

Definitions and Theorems

Function: definition-theory-rec

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

Function: definition-theory

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