Zulip Chat Archive

Stream: general

Topic: notation keyword


Edward Ayers (Feb 10 2019 at 14:06):

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

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

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

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

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

Edward Ayers (Feb 10 2019 at 15:59):

Hi Kevin I can't follow your link

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

Sorry, kill the Or

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

remove the Or

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

I'll edit

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

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: Aug 03 2023 at 10:10 UTC