为什么变量 x 可以并且必须在函数定义的左侧出现两次？意义何在？

问题描述

我是 Idris 的新手，对这个定义感到困惑，因为我不明白它是如何工作的。 定义如下。

sameS : (k : Nat)->(j : Nat)->(k = j)->((S k) = (S j))
sameS x x Refl=Refl

解决方法

让我们从分解类型签名开始：

sameS : (k : Nat) -> (j : Nat) -> (k = j) -> ((S k) = (S j))

sameS 是一个函数。 sameS 采用以下参数：

1. (k : Nat) 一个 k 类型的参数 Nat
2. (j : Nat) 类型为 j 的参数 Nat
3. (k = j) k 和 j 相等的证明

sameS 返回：

((S k) = (S j)) 证明 S k 和 S j 相等。

现在让我们分解定义：

sameS x x Refl = Refl

Refl 的类型是 a = a。

x 既是第一个参数，又是第二个参数，因为它们是相同的。我们知道这一点是因为第三个参数是 Refl。

Refl 被返回，因为 S x = S x。