dependent-type - 为什么不涉及 Idris 中的 “minus” 类型检查的相等性？

Question

为什么不进行以下类型检查:

minusReduces : (n : Nat) -> n `minus` Z = n
minusReduces n = Refl

然而，这将很好地进行类型检查:

plusReduces : (n : Nat) -> Z `plus` n = n
plusReduces n = Refl

Answer 1

minus n不会减少，因为 minus是 defined在第一个参数上使用模式匹配:

total minus : Nat -> Nat -> Nat
minus Z        right     = Z
minus left     Z         = left
minus (S left) (S right) = minus left right

所以你需要拆分你的 Z和 S n情况也一样:

minusReduces : (n : Nat) -> n `minus` Z = n
minusReduces Z = Refl
minusReduces (S k) = Refl