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