相关疑难解决方法(0)

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

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

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

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

任何帮助表示赞赏。