Zulip Chat Archive

Stream: general

Topic: notation keyword


view this post on Zulip 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.

view this post on Zulip Edward Ayers (Feb 10 2019 at 14:15):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 15:48):

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

view this post on Zulip Edward Ayers (Feb 10 2019 at 15:59):

Hi Kevin I can't follow your link

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 16:00):

Sorry, kill the Or

view this post on Zulip Patrick Massot (Feb 10 2019 at 16:00):

remove the Or

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 16:00):

I'll edit

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 16:00):

I'm on phone

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 16:04):

Oh but that is just a hack

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 16:05):

Otherwise exists unique would work properly

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 16:06):

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

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 16:06):

Backwards E then !

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 16:06):

It iterates to the wrong thing

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Feb 10 2019 at 16:16):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 10 2019 at 16:21):

Wow, we were all so much younger then

view this post on Zulip 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

view this post on Zulip 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: May 10 2021 at 18:22 UTC