Как обновить значения переменных в ACL2?

Question

Я новичок в ACL2 доказатель теоремы. Я хочу обновить значение переменной на основе результата XOR трех переменных. Я думаю, что "setq" сделает это для меня.

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

Тем не менее, я получаю эту ошибку:

Ошибка ACL2 в верхнем уровне: символ SETQ (в пакете "COMMON-LISP") не имеет ни определения функции, ни макроопределения в ACL2. Более того, этот символ находится в основном пакете Lisp; следовательно, вы не можете определить его в ACL2. Смотрите:DOC почти не попадает. Примечание: эта ошибка произошла в контексте (SETQ OUT (XOR (XOR A B) C)).

Разве мы не можем использовать основные функции Lisp в ACL2? Есть ли другой способ обновить значения переменных в ACL2? Я уже пытался "назначить", но я не хочу, чтобы моя переменная стала глобальной.

Answer 1

ACL2 - это аппликативный язык программирования (на самом деле ACL2 расшифровывается как "Вычислительная логика для Applicative Common Lisp"), поэтому вы не можете изменять значения в своем коде; Вы можете связывать только новые. Так что возможно let или же let* это то, что вы ищете.