英文:
Output of #check Nat.add
问题
输出为
```#检查 Nat.add```
看起来混乱 - 结果如下
```Nat.add (a✝a✝¹ : Nat) : Nat```
版本：4.0.0-nightly-2023-07-06，提交 c268d7e97bb0，发布版
我该如何理解这个输出？
英文:
the output of
#check Nat.add
seems to be garbled - the result looks like
Nat.add (a✝a✝¹ : Nat) : Nat
Version: 4.0.0-nightly-2023-07-06, commit c268d7e97bb0, Release
How can I make sense of this output?
答案1
得分: 1
以下是翻译好的部分：
唯一不符合我们期望的输出部分（由于漂亮的打印机限制）是两个标识符之间缺少空格的部分；它应该是这样的：
Nat.add (a✝ a✝¹ : Nat) : Nat
它的意思是 Nat.add 是一个具有两个 Nat 类型参数的函数，它返回一个 Nat 类型的值。参数被赋予了名称，但这些名称本身是“卫生的”，即不能直接表达，这在漂亮的打印机中用标识符后面的一个†符号来表示。（这很可能表明该函数是在没有命名参数的情况下编写的，就像 def Nat.add : Nat -> Nat -> Nat := ... 一样。）如果函数已经声明为带有命名参数，你将在这里看到它们：
def foo (x y : Nat) : Nat := x + y
#check foo
-- foo (x y : Nat) : Nat
参数的名称很重要，因为你可以在代码中使用它们：
#check foo (y := 2) (x := 1)
-- foo 1 2 : Nat
英文:
The only part of that output that is actually not printed the way we would want (due to pretty printer limitations) is the lack of space between the two identifiers; it should have said:
Nat.add (a✝ a✝¹ : Nat) : Nat
What it means is that Nat.add is a function with two arguments of type Nat and which returns a value of type Nat. The arguments are given names, but the names themselves are "hygienic" a.k.a not expressible directly, which is indicated in the pretty printer using a dagger symbol after the identifier. (This most likely indicates that the function was written without naming the arguments, as in def Nat.add : Nat -> Nat -> Nat := ....) If the function had been declared with named parameters, you would see them here:
def foo (x y : Nat) : Nat := x + y
#check foo
-- foo (x y : Nat) : Nat
The names of the parameters are relevant because you can use them in code:
#check foo (y := 2) (x := 1)
-- foo 1 2 : Nat
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论