Included Books
other
(in-package "ACL2")
include-book
(include-book "fsublis-var")
include-book
(include-book "std/testing/assert-equal" :dir :system)
other
(assert-equal (fsublis-var '((x quote 1) (y quote 2)) ''"a") ''"a")
other
(assert-equal (fsublis-var '((x quote 1) (y quote 2)) 'z) 'z)
other
(assert-equal (fsublis-var '((x quote 1) (y quote 2)) 'x) ''1)
other
(assert-equal (fsublis-var '((x quote 1) (y quote 2)) '((lambda (x) x) y)) '((lambda (x) x) '2))
other
(assert-equal (fsublis-var '((x quote 1) (y quote 2)) '(f x (g z))) '(f '1 (g z)))