Часы GL ACL2 закончились

Question

Что это значит, когда я получаю следующее сообщение об ошибке? Я загрузил GL.

| ACL2 Error in ( DEFTHM SOME-THEOREM-THAT-USES-GL ...):  The clock
| ran out.~%

Answer 1

Скорее всего, пока вы загрузили GL, вы еще не определили процессор предложений, который включает в себя все необходимые символические аналоги. Это может произойти, даже если вы уже определили процессор предложений GL - вы, вероятно, включили некоторые другие книги после определения процессора предложений GL.

Чтобы решить эту проблему, просто определите еще один процессор предложения GL:

(def-gl-clause-processor yet-another-gl-clause-processor)