http://docs.idris-lang.org/en/v0.99/tutorial/theorems.html#totality-checking-issues指出:
Secondly, the current implementation has had limited effort put into it so far, so there may still be cases where it believes a function is total which is not. Do not rely on it for your proofs yet!
这是否意味着不能依赖 Idris 来提供证明，或者是否有办法创建不需要完整性检查器的证明？
最佳答案
所有证明助手都面临着实现错误(甚至是硬件错误!)的风险，这可能会使系统不一致并允许用户证明任何东西。这种风险永远不可能为零。即使我们证明了证明助手实现的正确性，该证明也必须在其他一些正式或非正式系统中得到证明，并面临相同的风险。
因此，我们应该从证明助手那里得到的并不是绝对正确的真理，而只是有效性的有力证据。该证据的强度取决于我们关于系统可信度的先前信息，以及我们能够在多大程度上查看特定证据并确定它是否利用了不一致之处。
因此， idris 证明的证据有多强并不是一个明确的案例。我想说，与非正式证明相比，它们相当强大。此外，Idris 证明的规模还没有达到 Agda 或特别是 Coq 证明的程度，因此它们很可能可以通过人工检查来检查“漏洞”。
关于proof - 如果 idris 认为事情可能是完整的，但事实并非如此， idris 可以用来证明吗？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/41113431/