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

【问题标题】：How can I prove a basic inequality in dependant type language我如何证明依赖类型语言中的基本不等式
【发布时间】：2021-05-25 17:23:32
【问题描述】：

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

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

我该怎么做？

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

【问题讨论】：

【解决方案1】：

使用impossible:

absurdity : 0 = 1 -> Void
absurdity Refl impossible

【讨论】：