notation keyword

Stream: general

[Edward Ayers]

Hi all are there any docs on how notation works in Lean 3.4.x? I was staring at notation f ` $ `:1 a:0 := f a and I realised there is more to it than I thought.

[Edward Ayers]

Also in init/core.lean, How come notation α × β := prod α β doesn't need backticks?

[Kevin Buzzard]

What's the subtlety with $? This says that $ has binding power 1 and is..umm..right associative. Lean's parser is a Pratt parser. https://xenaproject.wordpress.com/2019/01/20/a-word-on-bidmas/ . Or do you know all this and you're asking about a subtlety that I've missed?

[Kevin Buzzard]

I don't know the answer to the core question though

[Edward Ayers]

Hi Kevin I can't follow your link

[Kevin Buzzard]

Sorry, kill the Or

[Patrick Massot]

remove the Or

[Kevin Buzzard]

I'll edit

[Kevin Buzzard]

I'm on phone

[Kevin Buzzard]

Every piece of notation has a right binding power and, if infix, an associativity. In Lean the associativity is given by assigning two binding powers, one for the notation and one for the thing just after it. #print notation + and #print notation ^ to see the difference

[Edward Ayers]

I guess I'm just after some docs on the parser because I was thinking of writing some. Eg, when do you need backticks, explaining exactly how foldr works, what exactly are the keywords doing in notation `∃` binders `, ` r:(scoped P, Exists P) := r etc. I agree that you can usually figure it out by finding examples but I would like some definitive explanations.

[Kevin Buzzard]

Oh but that is just a hack

[Kevin Buzzard]

It's all going to change in Lean 4 and the cool stuff you want to do probably can't be done in Lean 3 anyway

[Kevin Buzzard]

Otherwise exists unique would work properly

[Kevin Buzzard]

You can't iterate the notation currently and this can't really be fixed

[Kevin Buzzard]

Backwards E then !

[Kevin Buzzard]

It iterates to the wrong thing

[Kevin Buzzard]

Simon Hudon once pointed out the relevant bit of the source code to me. I think they just hacked something together so that lists worked ([1,2,3]) and left it at that

[Kevin Buzzard]

My proudest Lean moment was when the core Lean people changed the associativity of ^ after I opened an issue

[Patrick Massot]

Ed, I think the fold conversation starts at https://gitter.im/leanprover_public/Lobby?at=5a5686366117191e614e3ce4

[Patrick Massot]

Unfortunately we didn't have threads at that time, so it's mixed with several other conversations

[Kevin Buzzard]

Wow, we were all so much younger then

[Kevin Buzzard]

Yes that was exactly the conversation I was thinking of! That was when I figured out what the point of Simon was. Before that he was just some guy asking incomprehensible questions

[Kevin Buzzard]

After that he was the guy that could actually make some sense of the source code