Search code examples
lean

Output of #check Nat.add

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

Solution

  • 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