Included Books
other
(in-package "ACL2")
include-book
(include-book "all-vars-open")
include-book
(include-book "std/testing/assert-bang" :dir :system)
include-book
(include-book "std/lists/sets" :dir :system)
other
(assert! (set-equiv (all-vars-open 'x) '(x)))
other
(assert! (set-equiv (all-vars-open 'y) '(y)))
other
(assert! (set-equiv (all-vars-open ''0) nil))
other
(assert! (set-equiv (all-vars-open '(f x (g y) z)) '(x y z)))
other
(assert! (set-equiv (all-vars-open '((lambda (z) (cons z z)) (f x))) '(x)))
other
(assert! (set-equiv (all-vars-open '((lambda (z) (cons z z)) (f y))) '(y)))