在ACL2中添加倒数

我有一个加起来等于n的函数,它是这样工作的

(defun sum-up-to-n (n)
(if (zp n)
       0
       (+ n (sum-up-to-n (- n 1)))))

倒数的平方是这样的

(defun sum-up-to-nSqRecip (n)
   (if (zp n)
       0
         (+  (sum-up-to-nSqRecip (- n 1))) 1/n^2) ))

我收到这个错误“的身体 SUM-UP-TO-NSQRECIP包含变量符号的自由引用 我不知道如何解决这个错误。

(encapsulate nil
  (set-state-ok t)
  (program)
  (defun check-expect-fn (left right sexpr state)
    (if (equal left right)
      (mv nil (cw "check-expect succeeded: ~x0~%" sexpr) state)
      (er soft nil "check-expect failed: ~x0
      Expected: ~x1
      Actual:   ~x2" sexpr right left)))
  (defmacro check-expect (&whole sexpr left right)
    `(check-expect-fn ,left ,right (quote ,sexpr) state))
  (logic))

(include-book "doublecheck" :uncertified-okp t :dir :teachpacks)
(include-book "arithmetic-5/top" :uncertified-okp t :dir :system)