【发布时间】：2017-11-28 23:49:55
【问题描述】：
为什么不进行以下类型检查：
minusReduces : (n : Nat) -> n `minus` Z = n
minusReduces n = Refl
但这会很好地进行类型检查：
plusReduces : (n : Nat) -> Z `plus` n = n
plusReduces n = Refl
【问题讨论】：
标签： dependent-type idris
【发布时间】：2017-11-28 23:49:55
【问题描述】：
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
【讨论】：
-
它有效。虽然我仍然很困惑。有一个
minus left Z = left子句，我看不到它在第一个参数上是如何拆分的。 -
是的，但您首先必须通过
minus Z right案例才能到达那里！记住箱子是有序的。 -
有趣。该行为不同于 shapeless/Scala 中的隐式解析规则。