回答情况：
提问时间：
问题标签：
我正在尝试写一个绑定到半人马座ACL2 2-桥。到目前为止，我可以从以下顺序开始这座桥：
Bridge: bridge-worker-1: Uncaught error in worker thread:
Undefined function ACL2
浏览 3提问于2014-02-21得票数 1
回答已采纳
我是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函数吗？是
浏览 4提问于2017-11-15得票数 1
回答已采纳
当尝试使用ACL2 e将表单复制到ctrl+t shell缓冲区时，并且我已经在shell缓冲区中放置了时间$，则会出现一个错误，即无法粘贴表单。如何更改emacs宏，以便能够粘贴到已经具有的ACL2 shell缓冲区(时间$写入它们)？
浏览 3提问于2015-11-23得票数 1
回答已采纳
我试图用ACL2 (特别是ACL2s)编写一个函数，它接受一个列表和一个自然数，并在给定的索引处返回列表中的项。因此(选择(列表12，3) 2)将返回3。Body contract falsified in: 任何帮助都是非常感谢的！
浏览 3提问于2016-01-25得票数 1
回答已采纳
1回答
我必须在ACL2中使用排序的映射/索引结构。目前，我有以下几点：
( (key1 . (val1 val2)) (key2 . (val3)) (key3 .
浏览 2提问于2014-11-10得票数 0
ACL2退出代码137是什么意思？输出内容如下：top.cert seems to be missing
浏览 12提问于2015-06-04得票数 1
回答已采纳
1回答
我不知道如何调用一个函数n次才能在另一个函数中使用(defun right-shift (l)我需要写另一个函数，这个函数需要移位'(l) n次 (natp n)我甚至不确定我是否正确地启动了该函数，并且我不知道如何调用它n次。
浏览 5修改于2017-10-26得票数 1
| ACL2 Error in ( DEFTHM SOME-THEOREM-THAT-USES-GL ...): The clock
| ran out.~%
浏览 2提问于2015-11-05得票数 0
回答已采纳
在为ACL2构建书籍时，我得到了以下错误。我该怎么摆脱它呢？
Magic number checking on storable file failed at ../../lib/auto/Storable/_retrieve.al) line 380, at /<elided>/sw/acl2/books/build/certlib.pl line 1850
浏览 5修改于2014-09-03得票数 0
在使用ACL2时，我在emacs中遇到了一些奇怪的击键咒语，缓冲区中的一个区域变成了只读。是什么导致了这种情况？如何取消地域的只读标记？
浏览 6修改于2015-03-28得票数 0
在ACL2图书目录中，每当我尝试构建或清理图书时，都会收到一条错误消息，如下所示：
GNUmakefile:299: *** Books Sanity Check Failed. Stop.
浏览 0提问于2015-08-12得票数 0
所以我对acl2和lisp还比较陌生，我不知道用lisp做这件事的方法。我怎样才能达到我的评价呢？(缺点a.)我一直在考虑迭代器，但有人告诉我ACL2只使用递归 ;cons a (up to n)
;;;unit
浏览 2修改于2018-10-18得票数 1
回答已采纳
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号