Included Books
other
(in-package "ACL2")
include-book
(include-book "remove-dead-if-branches")
include-book
(include-book "std/testing/assert-equal" :dir :system)
other
(assert-equal (remove-dead-if-branches 'x) 'x)
other
(assert-equal (remove-dead-if-branches ''3) ''3)
other
(assert-equal (remove-dead-if-branches '(f a b)) '(f a b))
other
(assert-equal (remove-dead-if-branches '(if a
b
c))
'(if a
b
c))
other
(assert-equal (remove-dead-if-branches '(if 't a b)) 'a)
other
(assert-equal (remove-dead-if-branches '(if 'nil
a
b))
'b)
other
(assert-equal (remove-dead-if-branches '(if (if 't a b) x y)) '(if a x y))
other
(assert-equal (remove-dead-if-branches '(if (if 'nil
a
b)
x
y))
'(if b
x
y))
other
(assert-equal (remove-dead-if-branches '(if x
(if 't
a
b)
y))
'(if x
a
y))
other
(assert-equal (remove-dead-if-branches '(if x
(if 'nil
a
b)
y))
'(if x
b
y))
other
(assert-equal (remove-dead-if-branches '(if x
y
(if 't
a
b)))
'(if x
y
a))
other
(assert-equal (remove-dead-if-branches '(if x
y
(if 'nil
a
b)))
'(if x
y
b))
other
(assert-equal (remove-dead-if-branches '(g (if a
b
c)
y))
'(g (if a
b
c)
y))
other
(assert-equal (remove-dead-if-branches '(g (if 't b c) y)) '(g b y))
other
(assert-equal (remove-dead-if-branches '(if (not 'nil) a b)) 'a)