问题标签 [acl2]

当我收到以下错误消息时，这是什么意思？我已经加载了 GL。

当尝试使用 ctrl+te 将表单复制到我的 ACL2 shell 缓冲区中并且我已经在 shell 缓冲区中放置了一个 time$ 时，我收到一个关于无法粘贴表单的错误。如何更改 emacs 宏，以便我可以粘贴到已经有（time$ 写入其中的 ACL2 shell 缓冲区？

使用 acl2，我试图创建一个函数“ins”，它递归地将第一个参数（一个列表）附加到第二个参数（另一个列表）中每个元素的前面，其中

返回

所以调用函数本身

会给我们

我提出了仅适用于包含单个元素的 arg2 列表的非递归函数，检查是否为空。

当我尝试提出一些递归的方法时，它将第一个参数附加到第二个参数列表中的所有元素上，我能做的最好的就是

但无论如何我总是得到零，我似乎无法弄清楚为什么。因此，我什至不知道我的递归调用是否正确。我只是很难跟踪非平凡的递归。

当我打断已经出去吃午饭的证明时，我quick-and-dirty-subsumption-replacement-step在回溯中看到了。如何禁用该启发式？

我正在尝试在 ACL2（特别是 ACL2s）中编写一个函数，该函数接受一个列表和一个自然数，并在给定索引处返回列表中的项目。所以 (select (list 1 2 3) 2) 将返回 3。

这是我的代码：

我收到以下错误：

任何帮助深表感谢！

我正在尝试在 ACL2 中以一元符号 ( O, (S O), (S (S O)), ...) 对自然数进行建模，并证明加法的交换性。这是我的尝试：

这可能不是最 LISPy 的方式，我习惯于使用模式匹配的语言。

我的问题正如评论所建议的那样：证明者循环，试图证明同一事物的越来越深的嵌套版本。我该如何阻止这个？该手册确实简要提到了循环重写规则，但没有说明如何处理它们。

我的期望是这个证明会失败，给我提示需要哪些辅助引理来完成它。我可以使用循环证明的输出来找出可能停止循环的引理吗？

在 ACL2 宏转换器中，是否可以将函数定义提升到顶层？

我正在尝试设计一个可以在给定函数时let-map定义如下函数的宏。map-doubledouble

如果我只关心顶层，我可以用define-map宏来做到这一点。但是，我希望这个宏能够在嵌套在另一个表达式中的上下文中调用。例如：

我希望let-map宏定义一个函数map-double，然后返回正文的结果，在这种情况下调用(map-double (list 1 2 3)). 我尝试用 来定义它flet，但我的map-double函数是递归的，所以flet不起作用。

我会使用labels，但 ACL2 不支持它。

所以为了允许递归，我想将map-f（map-double在我使用这个宏时）的定义提升到顶层。这在 ACL2 宏系统中可能吗？

在像球拍这样的系统中，我会使用类似的功能syntax-local-lift-expression来做到这一点。那么ACL2中有类似的形式吗？

我正在使用最新版本的 ACL2 Sedan 研究“图论练习”示例。不幸的是，ACL2 不接受find-next-step功能。我已经检查了几次它是否正确输入并且它调用的所有功能都可用。输出摘要的第一部分：

产生反例，包括简化标尺以最大限度地提高反例的可重复性。以下函数定义对应于函数定义中的实际循环，CCG 分析无法证明在所有情况下都终止：

作为一个新手，在我自己找出问题所在之前，我想确保本书的文本应该在轿车版本上运行。我也可能不知道一些必要的设置和书籍内容。任何帮助，将不胜感激。

ACL2 没有证明以下定理：

我的猜测是应该应用一个在奇数上加二的归纳方案：

该定理仍未被接受。非常感谢我在哪里出错或过于乐观的解释。

添加：

由于这个类似的定理在没有归纳提示的情况下被接受，我怀疑 thm-0 有其他问题。

我需要尝试展示一个找到列表最小值的函数，我觉得我快要得到它但实际上无法得到它。

导师给了我们这个功能：

然后说

然后我做了：

Proof Pad 中的哪个给了我一个错误，我无法弄清楚我做错了什么。

错误是：

硬 ACL2 错误：缺少 N 的 :value 参数

TOP-LEVEL 中的 ACL2 错误：尝试对表单进行宏扩展

宏体的评估导致以下错误：

评估中止。要调试，请参见 :DOC print-gv，参见 :DOC 跟踪，并参见 :DOC wet。