let keyword and fun expression?

Stream: new members

[Lingyin Luo]

Hello!
I'm new to lean and going through the book Theorem proving in Lean.
In chapter 2 Dependent Typesthere's an example to illustrate the difference of local definition using let and fun.

def foo := let a := Nat; fun x : a => x + 2

def bar := (fun a => fun x : a => x + 2) Nat

The first example type checks, while the second example cannot compile, and the info view gives me the information that failed to synthesize instance HAdd a Nat (?m.1936 a x).

And I also don't quite understand the second example here. Could someone explain it to me?
Thanks in advance!

[Edward van de Meent]

in order for lean to make (fun a => fun x : a => x + 2) Nat work, it first needs to "translate" what (fun a => fun x : a => x + 2) means. in order to do that, it needs to know what x + 2 means for all types a that could be passed to this function. the info view complains about the fact that it doesn't know that; + is defined via instances HAdd a b c, where (. + .) takes type a on the left, b on the right, and returns type c.

[Edward van de Meent]

the first example doesn't have this problem, because the inner x + 2 part is able to find out that a is equal to Nat, and there is an instance HAdd Nat Nat Nat

[Edward van de Meent]

basically, lean is complaining in the second example that it doesn't "know" that a will mean Nat in this case

[Lingyin Luo]

Edward van de Meent said:

in order for lean to make (fun a => fun x : a => x + 2) Nat work, it first needs to "translate" what (fun a => fun x : a => x + 2) means. in order to do that, it needs to know what x + 2 means for all types a that could be passed to this function. the info view complains about the fact that it doesn't know that; + is defined via instances HAdd a b c, where (. + .) takes type a on the left, b on the right, and returns type c.

Ah Ok, now I understand the sentence from the book what exactly means : there are expressions of the form let a:= t1; t2 that cannot be expressed as (fun a => t2) t1.
Thank you!

[Eric Wieser]

I think this example is explained by #tpil

[Eric Wieser]

https://leanprover.github.io/theorem_proving_in_lean4/dependent_type_theory.html#local-definitions