Filtering...

map-tests

books/std/osets/map-tests

Included Books

map assert-bang
other
(in-package "ACL2")
include-book
(include-book "map")
include-book
(include-book "std/testing/assert-bang" :dir :system)
other
(set-verify-guards-eagerness 2)
other
(map-function (integerp x))
other
(assert! (equal (map<integerp> '(1 2 3)) '(t)))
other
(assert! (equal (map-list<integerp> '(1 a 2 b)) '(t nil t nil)))
squarefunction
(defun square
  (x)
  (declare (xargs :guard t))
  (* (rfix x) (rfix x)))
other
(map-function (square x))
other
(assert! (equal (map<square> '(1 2 3)) '(1 4 9)))
other
(assert! (equal (map<square> '(a b c)) '(0)))
other
(map-function (square x) :in-package-of foo)
square-then-addfunction
(defun square-then-add
  (input offset)
  (declare (xargs :guard t))
  (+ (* (rfix input) (rfix input)) (rfix offset)))
other
(map-function (square-then-add input offset)
  :in-package-of foo)
other
(assert! (equal (map<square-then-add> '(1 2 3) 5)
    '(6 9 14)))
plusfunction
(defun plus
  (x y)
  (declare (xargs :guard (and (integerp x) (rationalp y))))
  (+ x y))
other
(quantify-predicate (integerp x) :in-package-of defthm)
other
(map-function (plus arg1 arg2)
  :in-package-of defthm
  :set-guard ((all<integerp> ?set))
  :list-guard ((all-list<integerp> ?list))
  :element-guard ((integerp a))
  :arg-guard ((rationalp arg2)))
other
(assert! (equal (map<plus> '(1 2 3) 1) '(2 3 4)))