相关疑难解决方法(0)

在 Agda 中玩证明验证时，我意识到我对某些类型明确使用了归纳原则，而在其他情况下则使用模式匹配。我终于在维基百科上找到了一些关于模式匹配和归纳原则的文字：“在 Agda 中，依赖类型模式匹配是该语言的一种原语，核心语言没有模式匹配转化为的归纳/递归原则。”

那么，由于 Agdas 模式匹配，Agda 中的类型理论归纳和递归原则（定义类型上的函数）是完全多余的吗？这样的东西（隐含路径归纳）那时只会有教学价值。

http://en.wikipedia.org/wiki/Agda_%28programming_language%29#Dependently_typed_pa​​ttern_matching

我无法弄清楚为什么我的路径归纳不是正确的类型检查.当提到C(refl x)时,它说"C x应该是一个函数类型,但它不是".也许我对refl的定义是错误的,或者我的{}和()有什么问题？

data _?_ {A : Set}(a : A) : A ? Set where
      refl : a ? a
infix 4 _?_

pathInd : ? {u} ? {A : Set} ? 
          (C : {x y : A} ? x ? y ? Set u) ? 
          (c : (x : A) ? C (refl x)) ? 
          ({x y : A} (p : x ? y) ? C p)
pathInd C c (refl x) = c x