find-events-tests

other

(in-package "ACL2")

include-book

(include-book "find-lemmas")

include-book

(include-book "std/lists/sets" :dir :system)

*p-def*constant

(defconst *p-def* '(defun p (x) x))

*q-def*constant

(defconst *q-def* '(defun q (x) (p x)))

*foo-def*constant

(defconst *foo-def* '(defthm foo (equal (p x) x)))

*bar-def*constant

(defconst *bar-def* '(defthm bar (equal (q x) (p x))))

local

(local (make-event *p-def*))

local

(local (make-event *q-def*))

local

(local (make-event *foo-def*))

local

(local (make-event *bar-def*))

local

(local (mutual-recursion (defun evenlp
      (x)
      (if (consp x)
        (oddlp (cdr x))
        t))
    (defun oddlp
      (x)
      (if (consp x)
        (evenlp (cdr x))
        nil))))

other

(assert-event (set-equiv (find-lemmas '(p)) (list *foo-def* *bar-def*)))

other

(assert-event (set-equiv (find-lemmas '(q)) (list *bar-def*)))

other

(assert-event (member-equal 'nth-update-nth
    (strip-cars (strip-cdrs (find-lemmas '(update-nth) nil)))))

other

(assert-event (not (member-equal 'nth-update-nth
      (strip-cars (strip-cdrs (find-lemmas '(update-nth)))))))

other

(assert-event (set-equiv (find-defs '(p)) (list *p-def* *q-def*)))

other

(assert-event (set-equiv (find-events '(p))
    (list *p-def* *q-def* *foo-def* *bar-def*)))

Included Books