试图证明以下断言:
equalityCommutesNat : (n : Nat) -> (m : Nat) -> n = m -> m = n
我在库中找到了 plusCommutes，但没有发现平等。
最佳答案
= 的唯一居民是 Refl : (a = a)，因此如果您进行模式匹配，您将获得 n 的证据> 是m。
这意味着您可以使用 Refl，因为 Idris 的模式匹配现在知道它们是相同的:
equalityCommutesNat : (n : Nat) -> (m : Nat) -> n = m -> m = n
equalityCommutesNat _ _ Refl = Refl
你可以在 REPL 中尝试一下:
> equalityCommutesNat 1 1 Refl
Refl : 1 = 1
关于idris - 如何证明 idris 的平等通勤？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/63124030/