Filtering...

dumb-occur-var-open-tests

books/std/system/dumb-occur-var-open-tests

Included Books

dumb-occur-var-open assert-bang
other
(in-package "ACL2")
include-book
(include-book "dumb-occur-var-open")
include-book
(include-book "std/testing/assert-bang" :dir :system)
other
(assert! (dumb-occur-var-open 'x 'x))
other
(assert! (not (dumb-occur-var-open 'x 'y)))
other
(assert! (not (dumb-occur-var-open 'x ''0)))
other
(assert! (dumb-occur-var-open 'y '(f x (g y) z)))
other
(assert! (dumb-occur-var-open 'x '((lambda (z) (cons z z)) (f x))))
other
(assert! (not (dumb-occur-var-open 'x '((lambda (z) (cons z z)) (f y)))))
other
(assert! (not (dumb-occur-var-open 'z '((lambda (z) (cons z z)) (f y)))))
other
(assert! (dumb-occur-var-open 'w '((lambda (z) (cons w z)) (f y))))
other
(assert! (not (dumb-occur-var-open 'z '((lambda (z) (cons w z)) (f y)))))