tail-recursive-p-tests

(in-package "ACL2")

(assert! (tail-recursive-p 'nthcdr (w state)))

(assert! (not (tail-recursive-p 'take (w state))))

(must-succeed* (defun fact
    (n)
    (declare (xargs :guard (natp n)))
    (if (zp n)
      1
      (* n (fact (1- n)))))
  (defun fact-tr
    (n acc)
    (declare (xargs :guard (and (natp n) (natp acc))))
    (if (zp n)
      acc
      (fact-tr (1- n) (* n acc))))
  (include-book "arithmetic/top-with-meta" :dir :system)
  (defthm fact-tr-correct-lemma
    (implies (natp acc)
      (equal (fact-tr n acc) (* acc (fact n)))))
  (defthm fact-tr-correct
    (equal (fact-tr n 1) (fact n))
    :hints (("Goal" :in-theory (disable fact-tr fact))))
  (assert! (not (tail-recursive-p 'fact (w state))))
  (assert! (tail-recursive-p 'fact-tr (w state))))