Filtering...

all-pkg-names-tests

books/std/system/all-pkg-names-tests

Included Books

all-pkg-names assert-equal
other
(in-package "ACL2")
include-book
(include-book "all-pkg-names")
include-book
(include-book "std/testing/assert-equal" :dir :system)
same-member-equalmacro
(defmacro same-member-equal
  (x y)
  `(let ((x ,X) (y ,Y))
    (and (subsetp-equal x y) (subsetp-equal y x))))
other
(assert-equal (all-pkg-names ''4) nil)
other
(assert-equal (all-pkg-names 'x) '("ACL2"))
other
(assert-equal (all-pkg-names '(binary-+ '5 'x)) '("ACL2"))
other
(assert! (same-member-equal (all-pkg-names '(car (binary-/ 'x)))
    (list "ACL2" *main-lisp-package-name*)))
other
(assert! (same-member-equal (all-pkg-names '(f abcde))
    (list "ACL2" "STD")))
other
(assert-equal (all-pkg-names '(deflist '8)) '("STD"))