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