了解`k:Nat ** 5 * k = n`签名 [英] Understanding `k : Nat ** 5 * k = n` Signature

问题描述

以下函数编译:

onlyModByFive : (n : Nat) -> (k : Nat ** 5 * k = n) -> Nat
onlyModByFive n k = 100

但是k用Nat ** 5 * k = n语法表示什么?

另外，我怎么称呼它?这是我尝试的方法，但我不理解输出.

Also, how can I call it? Here's what I tried, but I don't understand the output.

*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

推荐答案

(k : Nat) ** (5 * k = n)是由以下组成的从属对

(k : Nat) ** (5 * k = n) is a dependent pair consisting of

• 第一个元素k : Nat
• 第二个元素prf : 5 * k = n

• A first element k : Nat
• A second element prf : 5 * k = n

换句话说，这是一种存在类型，表示存在某些k : Nat这样的5 * k = n".为了具有建设性，您必须提供这样的k并证明它确实满足5 * k = n.

In other words, this is an existential type that says "there exists some k : Nat such that 5 * k = n". To be constructive, you must give such a k and a proof that it indeed satisfies 5 * k = n.

在您的示例中，如果将onlyModByFive部分应用于5，则会得到类型

In your example, if you partially apply onlyModByFive to 5, you get something of type

onlyModModByFive 5 : ((k : Nat) ** (5 * k = 5)) -> Nat

，因此第二个参数必须为(k : Nat) ** (5 * k = 5)类型.通过将k设置为1并证明5 * 1 = 5，我们只能在这里进行选择5 * 1 = 5:

so the second argument has to be of type (k : Nat) ** (5 * k = 5). There is only one choice of k we can make here, by setting it to 1, and proving that 5 * 1 = 5:

foo : Nat
foo = onlyModByFive 5 (1 ** Refl)

之所以可行，是因为5 * 1简化为5，因此我们必须证明5 = 5，这可以通过直接使用Refl : a = a(统一a ~ 5)简单地完成.

This works because 5 * 1 reduces to 5, so we have to prove 5 = 5, which can be trivially done by using Refl : a = a directly (unifying a ~ 5).

这篇关于了解`k:Nat ** 5 * k = n`签名的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！