Included Books
other
(in-package "ACL2")
include-book
(include-book "if-tree-leaf-terms")
include-book
(include-book "std/testing/assert-equal" :dir :system)
other
(assert-equal (if-tree-leaf-terms 'x) '(x))
other
(assert-equal (if-tree-leaf-terms ''1) '('1))
other
(assert-equal (if-tree-leaf-terms '(f x y)) '((f x y)))
other
(assert-equal (if-tree-leaf-terms '(if a
b
c))
'(b c))
other
(assert-equal (if-tree-leaf-terms '(if (if x
y
z)
b
c))
'(b c))
other
(assert-equal (if-tree-leaf-terms '(if a
(if x
y
z)
c))
'(y z c))
other
(assert-equal (if-tree-leaf-terms '(if a
(if x
y
z)
c))
'(y z c))