Filtering...

get-ruler-extenders-tests

books/std/system/get-ruler-extenders-tests

Included Books

get-ruler-extenders assert-equal must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "get-ruler-extenders")
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-ruler-extenders 'len (w state))
  *basic-ruler-extenders*)
other
(must-succeed* (defun f
    (x)
    (declare (xargs :ruler-extenders (cons)))
    (cons 3
      (if (consp x)
        (f (cdr x))
        nil)))
  (assert-equal (get-ruler-extenders 'f (w state)) '(cons)))
other
(must-succeed* (defun f
    (x)
    (declare (xargs :ruler-extenders :all))
    (cons 3
      (if (consp x)
        (f (cdr x))
        nil)))
  (assert-equal (get-ruler-extenders 'f (w state)) :all))
other
(must-succeed* (defun fact
    (n)
    (declare (xargs :ruler-extenders (:lambdas)))
    (the (integer 1 *)
      (if (posp n)
        (* n (fact (1- n)))
        1)))
  (assert-equal (get-ruler-extenders 'fact (w state))
    '(:lambdas)))