Filtering...

all-free-bound-vars-tests

books/std/system/all-free-bound-vars-tests

Included Books

all-free-bound-vars assert-bang
other
(in-package "ACL2")
include-book
(include-book "all-free-bound-vars")
include-book
(include-book "std/testing/assert-bang" :dir :system)
same-member-eqmacro
(defmacro same-member-eq
  (x y)
  `(let ((x ,X) (y ,Y))
    (and (subsetp-eq x y) (subsetp-eq y x))))
other
(assert! (same-member-eq (all-free/bound-vars 'x) '(x)))
other
(assert! (same-member-eq (all-free/bound-vars ''3) nil))
other
(assert! (same-member-eq (all-free/bound-vars ''(1 2 3)) nil))
other
(assert! (same-member-eq (all-free/bound-vars '(f y zz)) '(y zz)))
other
(assert! (same-member-eq (all-free/bound-vars '((lambda (x) (cons x x)) '3))
    '(x)))
other
(assert! (same-member-eq (all-free/bound-vars '((lambda (x) (cons x x)) (g x)))
    '(x)))
other
(assert! (same-member-eq (all-free/bound-vars '((lambda (x) (cons x x)) (h y y)))
    '(x y)))