void - 我如何证明依赖类型语言中的基本不等式

Question

我想在 idris 中定义以下函数，以学习如何处理否定：

absurdity : 0 = 1 -> Void
absurdity = ?how

我该怎么做 ？

我可以创建一个空的 lambda 并让编译器找出这不相等吗？

标签： voididrisinequalitynegation

Answer 1

使用impossible：

absurdity : 0 = 1 -> Void
absurdity Refl impossible