【发布时间】：2017-08-01 13:38:51
【问题描述】：
可能它是基本的，但我不明白为什么以下函数为 fnc Nat 以及 fnc Integer 回答 1，它甚至不包含在模式中.
fnc : Type -> Integer
fnc Bool = 1
fnc Nat = 2
【问题讨论】：
标签： pattern-matching idris typecase
【发布时间】：2017-08-01 13:38:51
【问题描述】：
你不能在类型上进行模式匹配，你不应该这样做。当我编译你的代码时，我收到下一个错误：
warning - Unreachable case: fnc Nat
这已经在前面讨论过：
更新：
终于找到了更相关的问题和答案：
【讨论】：
-
@Shersh 感谢您提供最后一个链接！你能投票支持重新提出这个非常好的问题吗？我觉得它被关闭了很遗憾。
-
@AntonTrunov 我也这么认为。投票支持重新开放。