1; (defpkg "MY-PKG" '(defun cons))
2
3(in-package "MY-PKG")
4
5(defun f1 (x)
6  (cons x x))
7
8(defun f2 (x)
9  (acl2::append x x))
10
11(defun consts ()
12  '(x defun cons))
13
14#!acl2
15(defthm test0
16  (let ((lst (my-pkg::consts)))
17    (and (equal (car lst) 'my-pkg::x)
18         (not (equal (car lst) 'acl2::x))
19         (equal (cadr lst) 'my-pkg::defun)
20         (equal (cadr lst) 'acl2::defun)
21         (equal (cadr lst) 'common-lisp::defun)
22         (equal (caddr lst) 'my-pkg::cons)
23         (equal (caddr lst) 'acl2::cons)
24         (equal (caddr lst) 'common-lisp::cons)))
25  :rule-classes nil)
26
27#!acl2
28(defthm test1a
29  (equal (symbol-package-name 'my-pkg::c)
30         "MY-PKG")
31  :rule-classes nil)
32
33#!acl2
34(defthm test1b
35  (equal (symbol-name 'my-pkg::c)
36         "C")
37  :rule-classes nil)
38
39#!acl2
40(defthm test2a
41  (equal (symbol-package-name 'my-pkg::defun)
42         "COMMON-LISP")
43  :rule-classes nil)
44
45#!acl2
46(defthm test2b
47  (equal (symbol-name 'my-pkg::defun)
48         "DEFUN")
49  :rule-classes nil)
50
51#!acl2
52(defthm test3a
53  (equal (symbol-package-name 'my-pkg::|defun|)
54         "MY-PKG")
55  :rule-classes nil)
56
57#!acl2
58(defthm test3b
59  (equal (symbol-name 'my-pkg::|defun|)
60         "defun")
61  :rule-classes nil)
62
63#!acl2
64(defthm test4
65  (equal (intern-in-package-of-symbol "DEFUN" 'my-pkg::c)
66         (intern-in-package-of-symbol "DEFUN" 'common-lisp::c))
67  :rule-classes nil)
68
69#!acl2
70(defthm test5
71  (not (equal (intern-in-package-of-symbol "defun" 'my-pkg::c)
72              (intern-in-package-of-symbol "defun" 'common-lisp::c)))
73  :rule-classes nil)
74
75#!acl2
76(defthm test6
77  (not (equal (intern-in-package-of-symbol "D" 'my-pkg::c)
78              (intern-in-package-of-symbol "D" 'common-lisp::c)))
79  :rule-classes nil)
80
81; Test of quoted constants:
82
83(defun fun0 ()
84  '(a defun b))
85
86(defun fun1 ()
87  '(a defun b . c))
88
89(acl2::defthm
90 fun0-thm
91 (acl2::equal (fun0)
92              (cons 'a (cons 'defun (cons 'b acl2::nil)))))
93
94(acl2::defthm
95 fun1-thm
96 (acl2::equal (fun1)
97              (cons 'a (cons 'defun (cons 'b 'c)))))
98