Filtering...

classes-tests

books/std/system/classes-tests

Included Books

classes assert-equal must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "classes")
include-book
(include-book "std/testing/assert-equal" :dir :system)
include-book
(include-book "std/testing/must-succeed-star" :dir :system)
other
(assert-equal (classes 'car-cdr-elim (w state)) '((:elim)))
other
(must-succeed* (defthm th (acl2-numberp (- x)))
  (assert-equal (classes 'th (w state)) '((:rewrite))))
other
(must-succeed* (defthm th
    (booleanp (if x
        t
        nil))
    :rule-classes :type-prescription)
  (assert-equal (classes 'th (w state))
    '((:type-prescription :typed-term (if x
         't
         'nil)))))