【发布时间】：2025-09-23 00:55:02
【问题描述】：
我想在idris中定义如下函数，学习如何处理否定：
absurdity : 0 = 1 -> Void
absurdity = ?how
我该怎么做？
我可以创建一个空的 lambda 并让编译器找出这不相等吗？
【问题讨论】：
标签： void idris inequality negation
【发布时间】：2025-09-23 00:55:02
【问题描述】：
使用impossible:
absurdity : 0 = 1 -> Void
absurdity Refl impossible
【讨论】：
-
这个关键字的文档记录不够好，很遗憾。不过谢谢！