1

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

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

但是，我收到此错误：

TOP-LEVEL 中的 ACL2 错误：符号 SETQ（在包“COMMON-LISP”中）在 ACL2 中既没有函数也没有宏定义。此外，这个符号在 Lisp 主包中；因此，您不能在 ACL2 中定义它。请参阅：DOC 未遂事件。注意：这个错误发生在上下文（SETQ OUT (XOR (XOR AB) C)）中。

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

4

1 回答 1

1

ACL2 是一种应用程序编程语言（实际上 ACL2 代表“A Computational Logic for Applicative Common Lisp”），因此您不能在代码中改变值；你只能绑定新的。所以也许let或者let*是你正在寻找的东西。

于 2018-02-21T00:14:13.143 回答