为什么伊德里斯没有涉及"减去"类型检查的平等？

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被定义与第一参数模式匹配:

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