如何解决为什么变量 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
采用以下参数:
-
(k : Nat)
一个k
类型的参数Nat
-
(j : Nat)
类型为j
的参数Nat
-
(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
。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。