1; A trivial test, but with macros called in bodies and some stuff that should 2; be ignored. 3 4(in-package "ACL2") 5 6(defmacro my-cons (x y) 7 `(cons ,x ,y)) 8 9(defun foo (x) 10 (my-cons x x)) ; macro call 11 12(defthm foo-prop 13 (equal (first (foo x)) ; macro call 14 x)) 15 16(set-bogus-mutual-recursion-ok t) ; should be ignored for translation 17 18(mutual-recursion 19 (defun bar (x) 20 (declare (xargs :measure (acl2-count x))) ; should be ignored for translation 21 (if (consp x) 22 (bar (cdr x)) 23 x)) 24 (defun h (x) 25 x)) 26