eval-events-from-file-test

Included Books

other

(in-package "ACL2")

include-book

(include-book "eval-events-from-file")

other

(eval-events-from-file "eval-events-from-file-test-data.lsp")

other

(set-enforce-redundancy t)

f1function

(defun f1 (x) (cons x x))

*c*constant

(defconst *c* (expt 2 3))

f1-*c*-valtheorem

(defthm f1-*c*-val (equal (f1 *c*) '(8 . 8)))