Idris 中类型的模式匹配

Question

可能它是基本的，但我不明白为什么以下函数对于fnc Nat以及fnc Integer回答 1 ，它甚至没有作为模式包含在内。

fnc : Type -> Integer
fnc Bool = 1
fnc Nat = 2

Answer 1

您不能对类型进行模式匹配，也不应该这样做。当我编译你的代码时，我收到下一个错误：

warning - Unreachable case: fnc Nat

这一点之前已经讨论过了：

1. 老讨论了。
2. 一些类似的问题。
3. GitHub 上有一些类似的问题。

更新：

终于找到了更相关的问题和答案：

为什么打字是一件坏事？