Filtering...

termfnp-tests

books/std/system/termfnp-tests

Included Books

termfnp assert-bang must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "termfnp")
include-book
(include-book "std/testing/assert-bang" :dir :system)
include-book
(include-book "std/testing/must-succeed-star" :dir :system)
other
(assert! (not (termfnp "cons" (w state))))
other
(assert! (not (termfnp 'fffffffff (w state))))
other
(assert! (termfnp 'cons (w state)))
other
(assert! (termfnp 'len (w state)))
other
(assert! (not (termfnp 'car-cdr-elim (w state))))
other
(must-succeed* (defun h (x) x)
  (assert! (termfnp 'h (w state))))
other
(assert! (termfnp '(lambda (x y) (binary-+ x (len (cons '3 'nil))))
    (w state)))
other
(assert! (not (termfnp '(lambda (x) (fffff x)) (w state))))