Idris 中不可能的模式
Impossible patterns in Idris
我正在学习 Idris，我被困在一个非常简单的引理上，该引理表明某些特定索引对于数据类型是不可能的。我尝试使用不可能的模式，但 Idris 拒绝使用它们并显示以下错误消息：
RegExp.idr line 32 col 13:
hasEmptyZero prf is a valid case
完整的代码片段在以下要点中可用：
https://gist.github.com/rodrigogribeiro/f27f1f035e5a98f506ee
感谢任何帮助。
我和 freenode Idris 社区的人谈过，他们向我解释说
荒谬的模式需要一个明确的不可能的案例才能检测到这真的是不可能的。例如：
hasEmptyZero : HasEmpty Zero -> Void
hasEmptyZero HasEps impossible
此处放置构造函数 HasEps 有助于 Idris 检测它不能用于构造类型 HasEmpty Zero 的值。完整（有效）代码位于以下要点：
https://gist.github.com/rodrigogribeiro/5b39048df1d9ddc083ec
我正在学习 Idris，我被困在一个非常简单的引理上，该引理表明某些特定索引对于数据类型是不可能的。我尝试使用不可能的模式，但 Idris 拒绝使用它们并显示以下错误消息：
RegExp.idr line 32 col 13:
hasEmptyZero prf is a valid case
完整的代码片段在以下要点中可用：
https://gist.github.com/rodrigogribeiro/f27f1f035e5a98f506ee
感谢任何帮助。
我和 freenode Idris 社区的人谈过，他们向我解释说 荒谬的模式需要一个明确的不可能的案例才能检测到这真的是不可能的。例如：
hasEmptyZero : HasEmpty Zero -> Void
hasEmptyZero HasEps impossible
此处放置构造函数 HasEps 有助于 Idris 检测它不能用于构造类型 HasEmpty Zero 的值。完整（有效）代码位于以下要点：
https://gist.github.com/rodrigogribeiro/5b39048df1d9ddc083ec