В Common Lisp есть map , который позволяет вам делать такие вещи: (map (lambda (x y) (/ x y)) (list 2 4 6 8 10 12) (list 1 2 3 4 5 6)) возвращение (2 2 2 2 2 2) Однако сейчас я работаю в ACL2, и нет такого понятия, как map . Поэтому,...

Как избежать сбоя низкоуровневого отладчика при компиляции ACL2 на SBCL? Вот сообщение об ошибке, которое я получаю при компиляции с использованием SBCL 1.2.3 в Linux: <snip> ACL2 loading '((COMP-FN :EXEC NIL "1" STATE)). NIL Finished...

Я пытаюсь понять сообщение об ошибке, чтобы рассмотреть возможность его исправления. Как правильно исправить следующую ошибку? Должен ли я добавить :oslib , :quicklisp и :quicklisp.osicat во включаемые книги внутри books/oslib/rmtree.lisp ?...

Как узнать, какие книги в настоящее время проходят сертификацию с помощью ACL2 на данной машине? Я знаю, что могу посмотреть на вывод и понять это, но это требует нетривиальных усилий.

Из каталога книг ACL2 всякий раз, когда я пытаюсь создать или очистить книги, я получаю сообщение об ошибке, которое выглядит так: GNUmakefile:299: *** Books Sanity Check Failed. Stop. Как я могу избежать этого сообщения об ошибке?

(defun listmover-fun (l n) (if (= n (len l))) (last l ) (position n 1) listmover-fun (l n+1) ) Пытаясь выяснить, как перебирать список в ACL2, я знаю, что это можно сделать в lisp, но я не могу использовать эти функции. Мы будем очень...