如何更新 ACL2 中的变量值？
How to update variable values in ACL2?
我是 ACL2 定理证明者的新手。我想根据三个变量的异或结果更新变量的值。我认为“setq”会为我做到这一点。
(setq out (xor (xor a b) c))
但是，我得到这个错误：
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)).
我们不能在 ACL2 中使用主要的 Lisp 函数吗？还有另一种方法可以更新 ACL2 中的变量值吗？我已经尝试过 "assign"，但我不想让我的变量成为全局变量。
ACL2 是一个 applicative programming language（实际上 ACL2 代表 "A Computational Logic for Applicative Common Lisp"），因此您不能在代码中更改值；你只能绑定新的。所以也许 let 或 let* 就是您要找的东西。
我是 ACL2 定理证明者的新手。我想根据三个变量的异或结果更新变量的值。我认为“setq”会为我做到这一点。
(setq out (xor (xor a b) c))
但是，我得到这个错误：
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)).
我们不能在 ACL2 中使用主要的 Lisp 函数吗？还有另一种方法可以更新 ACL2 中的变量值吗？我已经尝试过 "assign"，但我不想让我的变量成为全局变量。
ACL2 是一个 applicative programming language（实际上 ACL2 代表 "A Computational Logic for Applicative Common Lisp"），因此您不能在代码中更改值；你只能绑定新的。所以也许 let 或 let* 就是您要找的东西。