Filtering...

number-of-results-plus-tests

books/std/system/number-of-results-plus-tests

Included Books

number-of-results-plus assert-equal must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "number-of-results-plus")
include-book
(include-book "std/testing/assert-equal" :dir :system)
include-book
(include-book "std/testing/must-succeed-star" :dir :system)
other
(assert-equal (number-of-results+ 'cons (w state)) 1)
other
(assert-equal (number-of-results+ 'len (w state)) 1)
other
(must-succeed* (defun f (x) (mv x (list x)))
  (assert-equal (number-of-results+ 'f (w state)) 2))
other
(must-succeed* (defun f (x) (mv x (list x) (list x x)))
  (assert-equal (number-of-results+ 'f (w state)) 3))