term-possible-numbers-of-results-tests

Included Books

term-possible-numbers-of-results assert-equal must-succeed-star

other

(in-package "ACL2")

include-book

(include-book "term-possible-numbers-of-results")

include-book

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

include-book

(include-book "std/testing/must-succeed-star" :dir :system)

other

(assert-equal (term-possible-numbers-of-results 'x (w state))
  (list 1))

other

(assert-equal (term-possible-numbers-of-results ''3 (w state))
  (list 1))

other

(must-succeed* (defun f (x) (mv x x x))
  (assert-equal (term-possible-numbers-of-results '(f x) (w state))
    (list 3)))

other

(assert-equal (term-possible-numbers-of-results '(cons a (cons b 'nil))
    (w state))
  (list 1 2))

other

(must-succeed* (defun f (x) (mv x x))
  (assert-equal (term-possible-numbers-of-results '(if something
        (cons a (cons b 'nil))
        (f c))
      (w state))
    (list 2)))