acl2 - ACL2 的 GL 时钟用完了

Question

当我收到以下错误消息时，这是什么意思？我已经加载了 GL。

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

score 0 · Accepted Answer

很可能当您加载了 GL 时，您还没有定义一个包含所有必要符号对应项的子句处理器。即使您已经定义了 GL 子句处理器，也可能发生这种情况——您可能在定义 GL 子句处理器后已经包含了一些其他书籍。

要解决它，只需定义另一个 GL 子句处理器：

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

1 回答 1