Included Books
other
(in-package "ACL2")
include-book
(include-book "remove-progn")
include-book
(include-book "std/testing/assert-equal" :dir :system)
other
(assert-equal (remove-progn 'x) 'x)
other
(assert-equal (remove-progn ''#C(1 2)) ''#C(1 2))
other
(assert-equal (remove-progn '(f a b)) '(f a b))
other
(assert-equal (remove-progn '((lambda (x) (cons x x)) (g y))) '((lambda (x) (cons x x)) (g y)))
other
(assert-equal (remove-progn '(return-last 'progn (f x) (g y))) '(g y))
other
(assert-equal (remove-progn '(return-last 'progn x (return-last 'progn (f a b) (g c d)))) '(g c d))
other
(assert-equal (remove-progn '(return-last 'mbe1-raw a b)) '(return-last 'mbe1-raw a b))