Included Books
other
(in-package "ACL2")
include-book
(include-book "symbol-package-name-lst")
include-book
(include-book "std/testing/assert-equal" :dir :system)
other
(assert-equal (symbol-package-name-lst nil) nil)
other
(assert-equal (symbol-package-name-lst '(symbolp)) (list *main-lisp-package-name*))
other
(assert-equal (symbol-package-name-lst '(symbol-listp define deflist cons)) (list "ACL2" "ACL2" "STD" *main-lisp-package-name*))