idris - idris 中不可能的模式

Question

我正在学习 Idris 并且我陷入了一个非常简单的引理，该引理表明某些特定索引对于数据类型是不可能的。我尝试使用不可能的模式，但 Idris 拒绝使用以下错误消息:

RegExp.idr line 32 col 13:
hasEmptyZero prf is a valid case

完整的代码片段可在以下要点中找到:

https://gist.github.com/rodrigogribeiro/f27f1f035e5a98f506ee

任何帮助表示赞赏。

Answer 1

我和 freenode Idris 社区的人谈过，他们向我解释说
荒谬的模式需要一个明确的不可能的情况才能检测到那真的是不可能的。举个例子:

hasEmptyZero : HasEmpty Zero -> Void
hasEmptyZero HasEps impossible

在这里放置构造函数 HasEps帮助 Idris 检测到它不能用于构造 HasEmpty Zero 类型的值.完整(工作)代码的要点如下:

https://gist.github.com/rodrigogribeiro/5b39048df1d9ddc083ec