get-measure-plus-tests

Included Books

get-measure-plus assert-equal must-succeed-star

other

(in-package "ACL2")

include-book

(include-book "get-measure-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 (get-measure+ 'len (w state)) '(acl2-count 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 (get-measure+ 'f (w state))
    '(nfix (binary-+ '10 (unary-- x)))))