未解決のメタの原因を突き止める最善の方法は何ですか? 解決可能なすべての周囲のワイルドカードを拡張することにより、すべての未解決のメタ (および未解決のメタのみ) を穴に変える方法はありますか?
他に何もないとしても、未解決のメタを穴に変更すると、未解決のメタに関するメッセージが消えますか? それなら、メッセージが消えるまですべてのワイルドカードとすべての暗黙の引数を穴に変更してから、どれが問題を引き起こしているかを突き止めることができると思います...
質問する
808 次
1 に答える
5
1 つの方法 (必ずしも最良であるとは限りません) は、すべての暗黙的な引数を明示的なアンダースコアに置き換えることです。
f {_} {_} {_} (x {_} {_} {_})
この回答は Agda メーリング リストからのものです: https://lists.chalmers.se/pipermail/agda/2012/004123.html
于 2012-07-16T13:52:46.207 に答える