search

toelli-msft / lean4

Lean4 work in progress repo
Apache License 2.0
0 stars 0 forks source link

Incorrect syntax in funabst.md? #13

Open toelli-msft opened 3 years ago

toelli-msft commented 3 years ago

I started reading through the Lean 4 documentation. funabst.md contains the example fun (u : β) (z : α), u. Is this really correct Lean 4 syntax? Based on the preceeding documentation I was expecting fun (u : β) (z : α) => u. If it is correct syntax perhaps you could introduce it more explicitly, because I can't see where it is introduced.

toelli-msft commented 3 years ago

Seems like this was Lean 3 syntax:

We do not use , anymore to separate the binders from the lambda expression body

https://leanprover.github.io/lean4/doc/lean3changes.html