I am very new to ACL2 so I understand that some of you may feel this is such a simple solution that you would frown upon my outreach for help. I am trying to figure out how to get my code to add up to an Nth reciprocal squared (I.E if n=4 then i am looking for 1/1 + 1/4 + 1/9 + 1/16)
I have a function that will add up to n and it works and looks like this
(defun sum-up-to-n (n)
(if (zp n)
0
(+ n (sum-up-to-n (- n 1)))))
With the the Reciprocal squared looking like this
(defun sum-up-to-nSqRecip (n)
(if (zp n)
0
(+ (sum-up-to-nSqRecip (- n 1))) 1/n^2) ))
I receive this error "The body of SUM-UP-TO-NSQRECIP contains a free occurrence of the variable symbol |1/N^2|. Note that |1/N^2| occurs in the context of condition (NOT (ZP N)) from a surrounding IF test." and i do not know how to resolve this error.
included stuff
(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)
ACL2 uses LISP syntax, which means you need prefix operators. So 1/n^2 should be (/ 1 (* n n)).
LISP allows a lot of the characters to be in a name, 1/n^2 in your example is treated as a name of a variable, which isn't binded to anything (not an input either). This is why you are receiving the "free occurrence of the variable" error.