既阿格达和伊德里斯有效地禁止图案类型的值相匹配Type.似乎Agda总是在第一种情况下匹配,而Idris只是抛出一个错误.
那么,为什么typecase是一件坏事呢？它会破坏一致性吗？我无法找到有关该主题的更多信息.
我试图比较a String和String期待True.
Idris> String == String
Can't find implementation for Eq Type
然后我预计False在比较a String和a时Bool.
Idris> String /= Bool
Can't find implementation for Eq Type
我错过了import吗？