如何更新ACL2中的变量值？

Question

我是ACL2定理证明的新手。我想根据三个变量的XOR结果更新变量的值。我想“setq”会帮我做到的。

(setq out (xor (xor a b) c))

但是，我得到了以下错误：

顶层的ACL2错误:在ACL2中，符号SETQ (在软件包“COMMON”中)既没有函数也没有宏定义。此外，这个符号在主Lisp包中；因此，您不能在ACL2中定义它。你看，医生差一点就错过了。注意:此错误发生在上下文中(SETQ OUT (XOR (XOR )A、B) C)。

我们不能在ACL2中使用主要的Lisp函数吗？是否有另一种方法来更新ACL2中的变量值？我已经尝试过“分配”，但我不希望我的变量变成全局的。

Answer 1

ACL2是一个应用程序设计语言 (实际上ACL2代表的是“应用程序通用Lisp的计算逻辑”)，所以您不能在代码中修改值；您只能绑定新的值。所以也许let或let*就是你要找的东西。