Included Books
other
(in-package "ACL2")
include-book
(include-book "symbol-package-name-non-cl")
include-book
(include-book "std/testing/assert-equal" :dir :system)
other
(assert-equal (symbol-package-name-non-cl 'symbol-listp) "ACL2")
other
(assert-equal (symbol-package-name-non-cl 'define)
"ACL2")
other
(assert-equal (symbol-package-name-non-cl 'deflist)
"STD")
other
(assert-equal (symbol-package-name-non-cl 'cons) "ACL2")