http://docs.idris-lang.org/en/v0.99/tutorial/theorems.html#totality-checking-issuesには、次のように記載されています。
第 2 に、現在の実装ではこれまでの努力が限定的であったため、関数が total であると信じているがそうではない場合が依然としてある可能性があります。まだ証明のためにそれを当てにしないでください!
これは Idris を証明に当てにできないということですか、それとも全体性チェッカーを必要としない証明を作成する方法はありますか?