acl2

1熱度

1回答

我試圖在ACL2（特別是ACL2s）中編寫一個函數，該函數接受列表和自然數並返回給定索引處列表中的項。所以（選擇（表1 2 3）2）將返回3. 這裏是我的代碼： ;; select: List x Nat -> All (defunc select (l n) :input-contract (and (listp l) (natp n)) :output-contract

0熱度

1回答

ACL2的GL時鐘耗盡

當我收到以下錯誤消息時，這是什麼意思？我加載了GL。 | ACL2 Error in (DEFTHM SOME-THEOREM-THAT-USES-GL ...): The clock | ran out.~%

0熱度

1回答

禁用ACL2中的跳過警告警告

如何禁用ACL2中的跳過警告警告？包括故意有很多跳過證明的書籍可能會非常冗長。

0熱度

1回答

禁用過於多，IFS啓發式

如何禁用過於衆多，IFS啓發？有時候，證明者外出吃午飯，當我打斷它，我可以看到，證明是忙於too-many-ifs0和count-ifs-lst通話。

0熱度

1回答

如何在ACL2和emacs中使用ctrl + t e使時間$工作？

當使用ctrl + t e將表單複製到我的ACL2 shell緩衝區中，並且我已經在shell緩衝區中放置了一個時間$時，出現無法粘貼表單的錯誤。如何更改emacs的宏，以便我可以粘貼到已經有ACL2殼緩衝區（時間$寫進他們

0熱度

1回答

在構建ACL2書籍時，如何擺脫關於「幻數...」的錯誤

在構建ACL2書籍時，出現以下錯誤。我如何擺脫它？ Magic number checking on storable file failed at ../../lib/Storable.pm (autosplit into ../../lib/auto/Storable/_retrieve.al) line 380, at /<elided>/sw/acl2/books/build/certli

3熱度

1回答

在SBCL上編譯ACL2時，如何避免進入低級調試器？

在SBCL上編譯ACL2時，如何避免進入低級調試器？下面是在Linux上使用SBCL 1.2.3編譯時我收到錯誤消息： <snip> ACL2 loading '((COMP-FN :EXEC NIL "1" STATE)). NIL Finished loading '((COMP-FN :EXEC NIL "1" STATE)). *************************

0熱度

1回答

確定當前通過ACL2認證的書籍

如何查看哪些書籍正在通過給定機器上的ACL2認證？我知道我可以查看輸出結果並找出結果，但這需要付出不小的努力。

0熱度

1回答

如何修復循環重寫證明

我試圖在ACL2中以一元符號（O，(S O),(S (S O))，...）對自然數進行建模並證明加法的交換性。這裏是我的嘗試： ; a NATURAL is 'O or a list ('S n') where n' is a NATURAL (defun naturalp (n) (cond ((equal n 'O) t) (t (and (true-listp n)

0熱度

2回答

瞭解ttags錯誤

我試圖弄清楚錯誤消息，以便我可以考慮修復它。什麼是解決以下錯誤的正確方法？是否應將:oslib,:quicklisp和:quicklisp.osicat添加到books/oslib/rmtree.lisp以內的包含書籍？我的包含書形式是否錯誤？ ACL2 !>(include-book "oslib/top" :dir :system :ttags (oslib quicklisp qui