在 Agda 中玩证明验证时，我意识到我对某些类型明确使用了归纳原则，而在其他情况下则使用模式匹配。我终于在维基百科上找到了一些关于模式匹配和归纳原则的文字：“在 Agda 中，依赖类型模式匹配是该语言的一种原语，核心语言没有模式匹配转化为的归纳/递归原则。”
那么，由于 Agdas 模式匹配，Agda 中的类型理论归纳和递归原则（定义类型上的函数）是完全多余的吗？这样的东西（隐含路径归纳）那时只会有教学价值。
http://en.wikipedia.org/wiki/Agda_%28programming_language%29#Dependently_typed_pattern_matching