rune-enabledp-tests

Included Books

rune-enabledp assert-equal must-succeed-star

other

(in-package "ACL2")

include-book

(include-book "rune-enabledp")

include-book

(include-book "std/testing/assert-equal" :dir :system)

include-book

(include-book "std/testing/must-succeed-star" :dir :system)

other

(assert! (rune-enabledp '(:rewrite cons-car-cdr) state))

other

(must-succeed* (defthm th (acl2-numberp (+ x y)))
  (assert! (rune-enabledp '(:rewrite th) state)))

other

(must-succeed* (defthmd th (acl2-numberp (+ x y)))
  (assert! (not (rune-enabledp '(:rewrite th) state))))

other

(must-succeed* (defthm th
    (acl2-numberp (+ x y))
    :rule-classes :type-prescription)
  (assert! (rune-enabledp '(:type-prescription th) state)))

other

(must-succeed* (defthm th
    (acl2-numberp (+ x y))
    :rule-classes ((:rewrite :corollary (acl2-numberp (+ x y))) (:rewrite :corollary (acl2-numberp (+ y x)))))
  (assert! (rune-enabledp '(:rewrite th . 1) state))
  (assert! (rune-enabledp '(:rewrite th . 2) state)))

other

(must-succeed* (defthmd th
    (acl2-numberp (+ x y))
    :rule-classes ((:rewrite :corollary (acl2-numberp (+ x y))) (:rewrite :corollary (acl2-numberp (+ y x)))))
  (assert! (not (rune-enabledp '(:rewrite th . 1) state)))
  (assert! (not (rune-enabledp '(:rewrite th . 2) state))))