I’m new to ACL2 theorem prover. I want to update the value of a variable based on XOR result of three variables. I think “setq” will do that for me.
(setq out (xor (xor a b) c))
However, I get this error:
ACL2 Error in TOP-LEVEL: The symbol SETQ (in package "COMMON-LISP") has neither a function nor macro definition in ACL2. Moreover, this symbol is in the main Lisp package; hence, you cannot define it in ACL2. See :DOC near-misses. Note: this error occurred in the context (SETQ OUT (XOR (XOR A B) C)).
Can't we use main Lisp functions in ACL2? Is there another way to update variable values in ACL2? I have already tried "assign", but I don't want my variable to become global.
ACL2 is an applicative programming language (in fact ACL2 stands for "A Computational Logic for Applicative Common Lisp"), so you cannot mutate values in your code; you can only bind new ones. So perhaps let or let* is what you're looking for.