measured-subset-plus-tests

Included Books

measured-subset-plus assert-equal must-succeed-star

other

(in-package "ACL2")

include-book

(include-book "measured-subset-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 (measured-subset+ 'len (w state)) '(x))

other

(assert-equal (measured-subset+ 'binary-append (w state))
  '(x))

other

(must-succeed* (defun f
    (x)
    (declare (xargs :measure (nfix (- 10 x))))
    (if (and (natp x) (< x 10))
      (f (1+ x))
      nil))
  (assert-equal (measured-subset+ 'f (w state)) '(x)))

other

(must-succeed* (defun f
    (x y z)
    (declare (xargs :measure (nfix (- 10 y))))
    (if (and (natp y) (< y 10))
      (f x (1+ y) z)
      (cons x z)))
  (assert-equal (measured-subset+ 'f (w state)) '(y)))