## Stream: general

### Topic: notation keyword

#### Kevin Buzzard (Feb 10 2019 at 15:48):

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

#### Kevin Buzzard (Feb 10 2019 at 16:00):

Sorry, kill the Or

remove the Or

I'll edit

I'm on phone

#### Kevin Buzzard (Feb 10 2019 at 16:03):

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 (Feb 10 2019 at 16:04):

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 (Feb 10 2019 at 16:04):

Oh but that is just a hack

#### Kevin Buzzard (Feb 10 2019 at 16:05):

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 (Feb 10 2019 at 16:05):

Otherwise exists unique would work properly

#### Kevin Buzzard (Feb 10 2019 at 16:06):

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

#### Kevin Buzzard (Feb 10 2019 at 16:06):

Backwards E then !

#### Kevin Buzzard (Feb 10 2019 at 16:06):

It iterates to the wrong thing

#### Kevin Buzzard (Feb 10 2019 at 16:08):

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 (Feb 10 2019 at 16:10):

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

#### Patrick Massot (Feb 10 2019 at 16:16):

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

#### Patrick Massot (Feb 10 2019 at 16:16):

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

#### Kevin Buzzard (Feb 10 2019 at 16:21):

Wow, we were all so much younger then

#### Kevin Buzzard (Feb 10 2019 at 16:22):

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 (Feb 10 2019 at 16:23):

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

Last updated: Dec 20 2023 at 11:08 UTC