以下函数编译：
onlyModByFive : (n : Nat) -> (k : Nat ** 5 * k = n) -> Nat
onlyModByFive n k = 100
但有什么作用k以其代表Nat ** 5 * k = n syntax?
另外，我该如何称呼它？这是我尝试过的，但我不明白输出。
*Test> onlyModByFive 5 5
When checking an application of function Main.onlyModByFive:
(k : Nat ** plus k (plus k (plus k (plus k (plus k 0)))) = 5) is not a
numeric type
答案来源-https://groups.google.com/d/msg/idris-lang/ZPi9wCd95FY/eo3tRijGAAAJ https://groups.google.com/d/msg/idris-lang/ZPi9wCd95FY/eo3tRijGAAAJ
(k : Nat) ** (5 * k = n)是一个依赖对，由以下组成
- 第一个元素
k : Nat
- 第二个元素
prf : 5 * k = n
换句话说，这是一种存在主义类型，它说“存在一些k : Nat这样5 * k = n“。为了具有建设性，你必须给出这样的k并证明它确实满足5 * k = n.
在你的例子中，如果你部分申请onlyModByFive to 5，你会得到某种类型的东西
onlyModModByFive 5 : ((k : Nat) ** (5 * k = 5)) -> Nat
所以第二个参数必须是类型(k : Nat) ** (5 * k = 5)。只有一种选择k我们可以在这里通过将其设置为1，并证明5 * 1 = 5:
foo : Nat
foo = onlyModByFive 5 (1 ** Refl)
这有效是因为5 * 1减少到5，所以我们必须证明5 = 5，这可以通过使用轻松完成Refl : a = a直接（统一a ~ 5).
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
