returnspecs-tests

(in-package "STD")

(include-book "returnspecs")

(include-book "std/testing/assert-bang" :dir :system)

(assert! (equal (untranslate-and 'x) '(x)))

(assert! (equal (untranslate-and 't) '(t)))

(assert! (equal (untranslate-and '(if x
        y
        z))
    '((if x
       y
       z))))

(assert! (equal (untranslate-and '(if x
        y
        'nil))
    '(x y)))

(assert! (equal (untranslate-and '(if x
        (if a
          b
          c)
        'nil))
    '(x (if a
        b
        c))))

(assert! (equal (untranslate-and '(if x
        (if a
          b
          'nil)
        'nil))
    '(x a b)))