Filtering...

thm-formula-plus-tests

books/std/system/thm-formula-plus-tests

Included Books

thm-formula-plus assert-equal must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "thm-formula-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 (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))))