Filtering...

tests

books/std/obags/tests

Included Books

core assert-bang assert-equal
other
(in-package "ACL2")
include-book
(include-book "core")
include-book
(include-book "std/testing/assert-bang" :dir :system)
include-book
(include-book "std/testing/assert-equal" :dir :system)
other
(assert! (bagp nil))
other
(assert! (bagp '(4/5)))
other
(assert! (bagp '(5 68)))
other
(assert! (bagp '(x x)))
other
(assert! (bagp '(5 5 5 68)))
other
(assert! (bagp '("a" "bb" "c" "c")))
other
(assert! (not (bagp 44)))
other
(assert! (not (bagp '(2 1))))
other
(assert-equal (bfix nil) nil)
other
(assert-equal (bfix '(4/5)) '(4/5))
other
(assert-equal (bfix '(5 68)) '(5 68))
other
(assert-equal (bfix '(x x)) '(x x))
other
(assert-equal (bfix '(5 5 5 68)) '(5 5 5 68))
other
(assert-equal (bfix '("a" "bb" "c" "c"))
  '("a" "bb" "c" "c"))
bfix-test1theorem
(defthm bfix-test1 (equal (bfix 44) nil))
bfix-test2theorem
(defthm bfix-test2 (equal (bfix '(2 1)) nil))
other
(assert! (emptyp nil))
other
(assert! (not (emptyp '(4/5))))
other
(assert! (not (emptyp '(5 68))))
other
(assert! (not (emptyp '(x x))))
other
(assert! (not (emptyp '(5 5 5 68))))
other
(assert! (not (emptyp '("a" "bb" "c" "c"))))
other
(assert-equal (head '(4/5)) 4/5)
other
(assert-equal (head '(5 68)) 5)
other
(assert-equal (head '(x x)) 'x)
other
(assert-equal (head '(5 5 5 68)) 5)
other
(assert-equal (head '("a" "bb" "c" "c")) "a")
other
(assert-equal (tail '(4/5)) nil)
other
(assert-equal (tail '(5 68)) '(68))
other
(assert-equal (tail '(x x)) '(x))
other
(assert-equal (tail '(5 5 5 68)) '(5 5 68))
other
(assert-equal (tail '("a" "bb" "c" "c"))
  '("bb" "c" "c"))
other
(assert-equal (insert #\a nil) '(#\a))
other
(assert-equal (insert 0 '(4/5)) '(0 4/5))
other
(assert-equal (insert 2 '(4/5)) '(4/5 2))
other
(assert-equal (insert 1 '(5 68)) '(1 5 68))
other
(assert-equal (insert 5 '(5 68)) '(5 5 68))
other
(assert-equal (insert 68 '(5 68)) '(5 68 68))
other
(assert-equal (insert 'xx '(x x)) '(x x xx))
other
(assert-equal (insert "a" '(5 5 5 68))
  '(5 5 5 68 "a"))
other
(assert-equal (insert "bbb" '("a" "bb" "c" "c"))
  '("a" "bb" "bbb" "c" "c"))
other
(assert-equal (delete #\a nil) nil)
other
(assert-equal (delete 0 '(4/5)) '(4/5))
other
(assert-equal (delete 4/5 '(4/5)) nil)
other
(assert-equal (delete 1 '(5 68)) '(5 68))
other
(assert-equal (delete 5 '(5 68)) '(68))
other
(assert-equal (delete 68 '(5 68)) '(5))
other
(assert-equal (delete 'xx '(x x)) '(x x))
other
(assert-equal (delete "a" '(5 5 5 68)) '(5 5 5 68))
other
(assert-equal (delete 5 '(5 5 5 68)) '(5 5 68))
other
(assert-equal (delete "bbb" '("a" "bb" "c" "c"))
  '("a" "bb" "c" "c"))
other
(assert-equal (delete "c" '("a" "bb" "c" "c"))
  '("a" "bb" "c"))
other
(assert! (not (in '(7 3) nil)))
other
(assert! (not (in '(7 3) '(4/5))))
other
(assert! (in 4/5 '(4/5)))
other
(assert! (not (in 33 '(5 68))))
other
(assert! (in 5 '(5 68)))
other
(assert! (in 68 '(5 68)))
other
(assert! (not (in 'y '(x x))))
other
(assert! (in 'x '(x x)))
other
(assert! (not (in 6 '(5 5 5 68))))
other
(assert! (in 5 '(5 5 5 68)))
other
(assert! (in 68 '(5 5 5 68)))
other
(assert! (in "c" '("a" "bb" "c" "c")))
other
(assert-equal (occs '(7 3) nil) 0)
other
(assert-equal (occs '(7 3) '(4/5)) 0)
other
(assert-equal (occs 4/5 '(4/5)) 1)
other
(assert-equal (occs 33 '(5 68)) 0)
other
(assert-equal (occs 5 '(5 68)) 1)
other
(assert-equal (occs 68 '(5 68)) 1)
other
(assert-equal (occs 'y '(x x)) 0)
other
(assert-equal (occs 'x '(x x)) 2)
other
(assert-equal (occs 6 '(5 5 5 68)) 0)
other
(assert-equal (occs 5 '(5 5 5 68)) 3)
other
(assert-equal (occs 68 '(5 5 5 68)) 1)
other
(assert-equal (occs "c" '("a" "bb" "c" "c")) 2)
other
(assert-equal (cardinality nil) 0)
other
(assert-equal (cardinality '(4/5)) 1)
other
(assert-equal (cardinality '(5 68)) 2)
other
(assert-equal (cardinality '(x x)) 2)
other
(assert-equal (cardinality '(5 5 5 68)) 4)
other
(assert-equal (cardinality '("a" "bb" "c" "c")) 4)
other
(assert! (subbag nil nil))
other
(assert! (subbag nil '(4/5)))
other
(assert! (not (subbag '(4/5) nil)))
other
(assert! (subbag '(4/5) '(4/5)))
other
(assert! (subbag '(1 2 3) '(1 2 2 3)))
other
(assert! (not (subbag '(1 2 2 3) '(1 2 3))))
other
(assert-equal (union nil '(a b)) '(a b))
other
(assert-equal (union '(a b) nil) '(a b))
other
(assert-equal (union '(a b) '(c c d)) '(a b c c d))
other
(assert-equal (intersect nil '(a b)) nil)
other
(assert-equal (intersect '(a b) nil) nil)
other
(assert-equal (intersect '(a b) '(c c d)) nil)
other
(assert-equal (intersect '(a b) '(b b c c d)) '(b))
other
(assert-equal (difference nil '(a b)) nil)
other
(assert-equal (difference '(a b) nil) '(a b))
other
(assert-equal (difference '(a b) '(c c d)) '(a b))
other
(assert-equal (difference '(a b) '(b b c c d)) '(a))