Filtering...

quantify-tests

books/std/osets/quantify-tests

Included Books

quantify assert-bang
other
(in-package "ACL2")
include-book
(include-book "quantify")
include-book
(include-book "std/testing/assert-bang" :dir :system)
other
(quantify-predicate (integerp x))
other
(quantify-predicate (symbolp x))
other
(quantify-predicate (rationalp x))
other
(quantify-predicate (natp x))
other
(assert! (all<integerp> '(1 2 3)))
other
(assert! (all<not-integerp> '(a b c)))
other
(assert! (equal (find<symbolp> '(1 2 3 a b c)) 'a))
other
(quantify-predicate (eqlablep x) :in-package-of defthm)
other
(assert! (exists<eqlablep> '(c (a . b))))
lesspfunction
(defun lessp
  (a b)
  (declare (xargs :guard t))
  (< (rfix a) (rfix b)))
other
(quantify-predicate (lessp a b))
other
(assert! (all<lessp> '(1 2 3) 6))
other
(assert! (not (all<lessp> '(1 2 3) 2)))
fast-lesspfunction
(defun fast-lessp
  (a b)
  (declare (xargs :guard (and (rationalp a) (rationalp b))))
  (< a b))
other
(quantify-predicate (fast-lessp x max)
  :set-guard ((all<rationalp> ?set))
  :list-guard ((all-list<rationalp> ?list))
  :arg-guard ((rationalp max))
  :in-package-of defthm)
other
(assert! (equal (find<fast-lessp> '(-10 -5 0 5 10) 100) -10))
in-theory
(in-theory (disable theory<integerp>))
in-theory
(in-theory (disable theory<fast-lessp>))
unguarded-morepfunction
(defun unguarded-morep (a b) (> a b))
other
(quantify-predicate (unguarded-morep x max)
  :verify-guards nil)
other
(assert! (equal (find<unguarded-morep> '(1 2 3 4 5 6 7) 5) 6))