Included Books
other
(in-package "ACL2")
include-book
(include-book "untranslate-dollar")
include-book
(include-book "std/testing/assert-equal" :dir :system)
other
(assert-equal (untranslate$ 'x nil state) 'x)
other
(assert-equal (untranslate$ ''4 nil state) 4)
other
(assert-equal (untranslate$ ''"abc" nil state) "abc")
other
(assert-equal (untranslate$ '(f x) nil state) '(f x))
other
(assert-equal (untranslate$ '((lambda (x) (binary-+ '1 x)) '3) nil state) '(let ((x 3)) (+ 1 x)))
other
(assert-equal (untranslate$ '(if a
b
'nil)
nil
state)
'(and a b))
other
(assert-equal (untranslate$ '(if a
a
b)
nil
state)
'(or a b))