Filtering...

non-executablep-plus-tests

books/std/system/non-executablep-plus-tests

Included Books

non-executablep-plus assert-bang must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "non-executablep-plus")
include-book
(include-book "std/testing/assert-bang" :dir :system)
include-book
(include-book "std/testing/must-succeed-star" :dir :system)
other
(assert! (not (non-executablep+ 'not (w state))))
other
(assert! (not (non-executablep+ 'len (w state))))
other
(must-succeed* (defun-nx f (x) x)
  (assert! (non-executablep+ 'f (w state))))
other
(must-succeed* (defun-sk g (x) (forall (y z) (equal x (cons y z))))
  (assert! (non-executablep+ 'g (w state))))
other
(must-succeed* (defun-sk h
    (x y)
    (declare (xargs :non-executable nil))
    (exists z (equal z (cons x y))))
  (assert! (not (non-executablep+ 'h (w state)))))