classes-plus-tests

Included Books

classes-plus assert-equal must-succeed-star

other

(in-package "ACL2")

include-book

(include-book "classes-plus")

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)))))