What does $ mean?

Stream: new members

[Patrick Lutz]

After doing some exercises on codewars and looking at the other solutions that people submitted to the problems I solved I noticed that some solutions use the symbol $. What does that symbol mean? I don't think it's explained in Theorem Proving in Lean or the other tutorials I've looked at

[Jalex Stark]

f $ .. is like f ( .. )

[Jalex Stark]

i think it's the same $ from haskell

[Patrick Lutz]

Oh, I see. Is there any reason to prefer one over the other?

[Patrick Lutz]

Or is it just to prevent build up of ('s?

[Jalex Stark]

right, it's just to prevent parentheses

[Jalex Stark]

especially ones where the two ends are far apart

[Jalex Stark]

for dumb reasons, $ doesn't work correctly in tactic mode

[Jalex Stark]

so i mostly don't use it

[Patrick Lutz]

What's the reason?

[Jalex Stark]

oh i don't know

[Jalex Stark]

something about special parsing used for interactive tactics or something

[Patrick Lutz]

I see. Thanks for answering my question btw

[Jalex Stark]

i tried to modify the assumption tactic to accept an optional assumption? and all hell broke loose

[Jalex Stark]

i think we're supposed to accept these things because they're getting fixed in lean 4 and they're not halting mathlib progress now

[Shing Tak Lam]

Jalex Stark said:

for dumb reasons, $ doesn't work correctly in tactic mode

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/term.20mode.20haveI/near/198705223

Essentially, $ has a really low precedence

[Kevin Buzzard]

You can see for yourself what any notation like $ does with #print notation $. To understand the output in this case you will need to know a little about Pratt parsers.

[Kevin Buzzard]

https://xenaproject.wordpress.com/2019/01/20/a-word-on-bidmas/