Collects all of the :DEFINITION runes from theory.
Function:
(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:
(defun definition-theory (theory) (declare (xargs :guard (true-listp theory))) (definition-theory-rec theory nil))