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?
Note: as of version 4.8 this change has been reverted, and the output looks like, as expected,
Nat.add : Nat → Nat → 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