Filtering...

tests

books/std/omaps/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! (mapp nil))
other
(assert! (mapp '(("key" . #\v))))
other
(assert! (mapp '((a . 1) (b . 2) (c . 3))))
other
(assert! (not (mapp "ab")))
other
(assert! (not (mapp '(1 2 3))))
other
(assert! (not (mapp '((2 . 4/5) (1 . 4/5)))))
other
(assert-equal (mfix nil) nil)
other
(assert-equal (mfix '(("key" . #\v)))
  '(("key" . #\v)))
other
(assert-equal (mfix '((a . 1) (b . 2) (c . 3)))
  '((a . 1) (b . 2) (c . 3)))
mfix-test1theorem
(defthm mfix-test1 (equal (mfix "ab") nil))
mfix-test2theorem
(defthm mfix-test2 (equal (mfix '(1 2 3)) nil))
mfix-test3theorem
(defthm mfix-test3
  (equal (mfix '((2 . 4/5) (1 . 4/5))) nil))
other
(assert! (emptyp nil))
other
(assert! (not (emptyp '(("key" . #\v)))))
other
(assert! (not (emptyp '((a . 1) (b . 2) (c . 3)))))
other
(assert-equal (mv-list 2 (head '(("key" . #\v))))
  '("key" #\v))
other
(assert-equal (mv-list 2 (head '((a . 1) (b . 2) (c . 3))))
  '(a 1))
other
(assert-equal (tail '(("key" . #\v))) nil)
other
(assert-equal (tail '((a . 1) (b . 2) (c . 3)))
  '((b . 2) (c . 3)))
other
(assert-equal (update '(8 8) 'x nil) '(((8 8) . x)))
other
(assert-equal (update "loop" 0 '(("key" . #\v)))
  '(("key" . #\v) ("loop" . 0)))
other
(assert-equal (update "abc" 0 '(("key" . #\v)))
  '(("abc" . 0) ("key" . #\v)))
other
(assert-equal (update 'aa -15 '((a . 1) (b . 2) (c . 3)))
  '((a . 1) (aa . -15) (b . 2) (c . 3)))
other
(assert-equal (update* nil '((a . 1) (b . 2) (c . 3)))
  '((a . 1) (b . 2) (c . 3)))
other
(assert-equal (update* '((d . 4)) '((a . 1) (b . 2) (c . 3)))
  '((a . 1) (b . 2) (c . 3) (d . 4)))
other
(assert-equal (update* '((a . 10) (d . 4))
    '((a . 1) (b . 2) (c . 3)))
  '((a . 10) (b . 2) (c . 3) (d . 4)))
other
(assert-equal (delete '(8 8) nil) nil)
other
(assert-equal (delete '(8 8) '(("key" . #\v)))
  '(("key" . #\v)))
other
(assert-equal (delete "key" '(("key" . #\v))) nil)
other
(assert-equal (delete "key" '((a . 1) (b . 2) (c . 3)))
  '((a . 1) (b . 2) (c . 3)))
other
(assert-equal (delete 'a '((a . 1) (b . 2) (c . 3)))
  '((b . 2) (c . 3)))
other
(assert-equal (delete 'b '((a . 1) (b . 2) (c . 3)))
  '((a . 1) (c . 3)))
other
(assert-equal (delete 'c '((a . 1) (b . 2) (c . 3)))
  '((a . 1) (b . 2)))
other
(assert-equal (delete 'd '((a . 1) (b . 2) (c . 3)))
  '((a . 1) (b . 2) (c . 3)))
other
(assert-equal (delete* '((8 8)) nil) nil)
other
(assert-equal (delete* '((8 8)) '(("key" . #\v)))
  '(("key" . #\v)))
other
(assert-equal (delete* '("key") '(("key" . #\v))) nil)
other
(assert-equal (delete* '("key") '((a . 1) (b . 2) (c . 3)))
  '((a . 1) (b . 2) (c . 3)))
other
(assert-equal (delete* '(#\g "key") '((a . 1) (b . 2) (c . 3)))
  '((a . 1) (b . 2) (c . 3)))
other
(assert-equal (delete* '(a) '((a . 1) (b . 2) (c . 3)))
  '((b . 2) (c . 3)))
other
(assert-equal (delete* '(b) '((a . 1) (b . 2) (c . 3)))
  '((a . 1) (c . 3)))
other
(assert-equal (delete* '(c) '((a . 1) (b . 2) (c . 3)))
  '((a . 1) (b . 2)))
other
(assert-equal (delete* '(d) '((a . 1) (b . 2) (c . 3)))
  '((a . 1) (b . 2) (c . 3)))
other
(assert-equal (delete* '(a b) '((a . 1) (b . 2) (c . 3)))
  '((c . 3)))
other
(assert-equal (delete* '(a b) '((a . 1) (b . 2) (c . 3) (d . 4)))
  '((c . 3) (d . 4)))
other
(assert-equal (assoc #\a nil) nil)
other
(assert-equal (assoc #\a '(("key" . #\v))) nil)
other
(assert-equal (assoc "key" '(("key" . #\v))) '("key" . #\v))
other
(assert-equal (assoc "key" '((a . 1) (b . 2) (c . 3))) nil)
other
(assert-equal (assoc 'a '((a . 1) (b . 2) (c . 3)))
  '(a . 1))
other
(assert-equal (assoc 'b '((a . 1) (b . 2) (c . 3)))
  '(b . 2))
other
(assert-equal (assoc 'c '((a . 1) (b . 2) (c . 3)))
  '(c . 3))
other
(assert! (not (in* '(#\a) nil)))
other
(assert! (not (in* '(#\a) '(("key" . #\v)))))
other
(assert! (in* '("key") '(("key" . #\v))))
other
(assert! (not (in* '("key") '((a . 1) (b . 2) (c . 3)))))
other
(assert! (in* '(a) '((a . 1) (b . 2) (c . 3))))
other
(assert! (in* '(b) '((a . 1) (b . 2) (c . 3))))
other
(assert! (in* '(c) '((a . 1) (b . 2) (c . 3))))
other
(assert! (in* '(a b) '((a . 1) (b . 2) (c . 3))))
other
(assert! (not (in* '("key" a) '((a . 1) (b . 2) (c . 3)))))
other
(assert-equal (lookup "key" '(("key" . #\v))) #\v)
other
(assert-equal (lookup 'a '((a . 1) (b . 2) (c . 3)))
  1)
other
(assert-equal (lookup 'b '((a . 1) (b . 2) (c . 3)))
  2)
other
(assert-equal (lookup 'c '((a . 1) (b . 2) (c . 3)))
  3)
other
(assert-equal (lookup* '("key") '(("key" . #\v)))
  '(#\v))
other
(assert-equal (lookup* '(a) '((a . 1) (b . 2) (c . 3)))
  '(1))
other
(assert-equal (lookup* '(b) '((a . 1) (b . 2) (c . 3)))
  '(2))
other
(assert-equal (lookup* '(c) '((a . 1) (b . 2) (c . 3)))
  '(3))
other
(assert-equal (lookup* nil '((a . 1) (b . 2) (c . 3)))
  nil)
other
(assert-equal (lookup* '(a b) '((a . 1) (b . 2) (c . 3)))
  '(1 2))
other
(assert-equal (lookup* '(b c) '((a . 1) (b . 2) (c . 3)))
  '(2 3))
other
(assert-equal (lookup* '(a c) '((a . 1) (b . 2) (c . 3)))
  '(1 3))
other
(assert-equal (lookup* '(a b c) '((a . 1) (b . 2) (c . 3)))
  '(1 2 3))
other
(assert-equal (rlookup #\v '(("key" . #\v))) '("key"))
other
(assert-equal (rlookup 10 '((a . 1) (b . 2) (c . 1)))
  nil)
other
(assert-equal (rlookup 1 '((a . 1) (b . 2) (c . 1)))
  '(a c))
other
(assert-equal (rlookup* '(#\v) '(("key" . #\v)))
  '("key"))
other
(assert-equal (rlookup* '(10) '((a . 1) (b . 2) (c . 1)))
  nil)
other
(assert-equal (rlookup* '(1) '((a . 1) (b . 2) (c . 1)))
  '(a c))
other
(assert-equal (rlookup* '(1 2) '((a . 1) (b . 2) (c . 1)))
  '(a b c))
other
(assert-equal (rlookup* '(1 2 3) '((a . 1) (b . 2) (c . 1)))
  '(a b c))
other
(assert-equal (rlookup* '(1 2 3) '((a . 1) (b . 2) (c . 3)))
  '(a b c))
other
(assert-equal (rlookup* '(1 2 3 "y") '((a . 1) (b . 2) (c . 3)))
  '(a b c))
other
(assert-equal (restrict nil '((a . 1) (b . 2) (c . 3)))
  nil)
other
(assert-equal (restrict '("x") '((a . 1) (b . 2) (c . 3)))
  nil)
other
(assert-equal (restrict '(a c) '((a . 1) (b . 2) (c . 3)))
  '((a . 1) (c . 3)))
other
(assert-equal (restrict '(c) '((a . 1) (b . 2) (c . 3)))
  '((c . 3)))
other
(assert-equal (restrict '(c (1 2)) '((a . 1) (b . 2) (c . 3)))
  '((c . 3)))
other
(assert-equal (keys nil) nil)
other
(assert-equal (keys '(("key" . #\v))) '("key"))
other
(assert-equal (keys '((a . 1) (b . 2) (c . 3)))
  '(a b c))
other
(assert-equal (values nil) nil)
other
(assert-equal (values '(("key" . #\v))) '(#\v))
other
(assert-equal (values '((a . 1) (b . 2) (c . 3))) '(1 2 3))
other
(assert-equal (values '((a . 30) (b . 20) (c . 25)))
  '(20 25 30))
other
(assert! (compatiblep nil nil))
other
(assert! (compatiblep nil '((a . 1) (b . 2) (c . 3))))
other
(assert! (compatiblep '((a . 1) (b . 2) (c . 3)) nil))
other
(assert! (compatiblep '((a . 1) (b . 2)) '((c . 3))))
other
(assert! (compatiblep '((a . 1) (b . 2)) '((a . 1) (c . 3))))
other
(assert! (not (compatiblep '((a . 1) (b . 2)) '((a . 2) (c . 3)))))
other
(assert! (submap nil nil))
other
(assert! (submap '((a . 1)) '((a . 1) (b . 55))))
other
(assert! (not (submap '((#\k . #\v)) nil)))
other
(assert! (submap '((a . 1) (c . 3)) '((a . 1) (b . 2) (c . 3))))
other
(assert! (not (submap '((a . 2) (c . 3)) '((a . 1) (b . 2) (c . 3)))))
other
(assert-equal (size nil) 0)
other
(assert-equal (size '((a . 1))) 1)
other
(assert-equal (size '((a . 1) (b . 2) (c . 3))) 3)
other
(assert-equal (from-lists nil nil) nil)
other
(assert-equal (from-lists '(a b) '(1 2))
  '((a . 1) (b . 2)))
other
(assert-equal (from-lists '(b a) '(2 1))
  '((a . 1) (b . 2)))
other
(assert-equal (from-lists '(a a) '(1 2)) '((a . 1)))
other
(assert-equal (from-alist nil) nil)
other
(assert-equal (from-alist '((a . 1) (b . 2)))
  '((a . 1) (b . 2)))
other
(assert-equal (from-alist '((b . 2) (a . 1)))
  '((a . 1) (b . 2)))
other
(assert-equal (from-alist '((a . 1) (a . 2)))
  '((a . 1)))