Filtering...

thm-formula-tests

books/std/system/thm-formula-tests

Included Books

thm-formula assert-equal must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "thm-formula")
include-book
(include-book "std/testing/assert-equal" :dir :system)
include-book
(include-book "std/testing/must-succeed-star" :dir :system)
other
(assert-equal (thm-formula 'car-cdr-elim (w state))
  '(implies (consp x) (equal (cons (car x) (cdr x)) x)))
other
(must-succeed* (defthm th (acl2-numberp (- x)))
  (assert-equal (thm-formula 'th (w state))
    '(acl2-numberp (unary-- x))))