0

次のエラー メッセージが表示されるのはどういう意味ですか? GLをロードしました。

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

1 に答える 1

0

GL をロードしている間、必要なすべてのシンボリック カウンターパートを含む節プロセッサをまだ定義していない可能性が最も高いです。これは、GL 句プロセッサを既に定義している場合でも発生する可能性があります。GL 句プロセッサを定義してから、他の本をいくつか含めている可能性があります。

それを解決するには、さらに別の GL 句プロセッサを定義するだけです。

(def-gl-clause-processor yet-another-gl-clause-processor)
于 2015-11-05T00:17:32.520 に答える