2

統合エラーを追跡するための :set showimplicits よりも有益なものはありますか? 私は現在これを取得していますが、ここからどこへ行くべきかわかりません:紛らわしい統合エラーのスクリーンショット

4

1 に答える 1

2

残念ながら、短い答えは「いいえ、そうではありません」です。ただし、悪いエラー メッセージが表示されるのは好きではないので、詳細を提供していただければ、調査して改善できる可能性があります。

より長い答えは、イドリスがここでエラーを報告する方法に問題があるということです。何が起こっているのかは次のようになると思います: https://github.com/idris-lang/Idris-dev/issues/2126

統一エラーの 2 番目の「具体的に」の部分のみを表示していることに気付きました。本当の問題はおそらく最初の部分にあります。統合の失敗は一時的なものであり、開発者がより多くの情報を入手したときに解決される可能性があるため、その追加情報が (通常は用語の他の部分から) 明らかになると、エラー メッセージが更新されます。ここで起こったことは、最初の試行で失敗した部分は今は大丈夫ですが、他の部分がまだ壊れているということです.

今のところ、「具体的に」という部分は無視して、最初の部分 (かなり大きいと思います) を見ることをお勧めします。あるいは、プログラムの関連部分が簡単に説明できる場合は、メーリング リストの誰かが助けてくれるでしょう。

最終的には関連する問題を修正する予定ですが...

于 2015-05-20T23:52:05.500 に答える