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

问题描述

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

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

我该怎么做？

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

解决方法

使用impossible：

absurdity : 0 = 1 -> Void
absurdity Refl impossible