可能它是基本的，但我不明白为什么以下函数为 fnc Nat 和 fnc Integer 回答 1，它甚至不作为模式包含在内。
fnc : Type -> Integer
fnc Bool = 1
fnc Nat = 2
最佳答案
您不能对类型进行模式匹配，也不应该这样做。当我编译你的代码时，我收到下一个错误:
warning - Unreachable case: fnc Nat
这在前面已经讨论过:
更新:
终于找到了更相关的问题和答案:
Why is typecase a bad thing?
关于pattern-matching - Idris 中类型的模式匹配，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/45439486/