Chaining dot notation

Stream: new members

[misterdrgn]

Hi all. A quick question, if you don't mind. I appreciate that Lean supports dot notation, but it seems like you'd have to use nested parentheses if you wanted to chain dot notation function calls.

#eval (((6: Nat).add 5).add 6).add 7

Is there another way to use dot notation that doesn't require nesting parentheses like this, or is dot notation in Lean not really meant for chaining?

Thanks.

[Matt Diamond]

check this out:

#eval 6 |>.add 5 |>.add 6 |>.add 7

[misterdrgn]

Matt Diamond said:

check this out:

#eval 6 |>.add 5 |>.add 6 |>.add 7

Ah, nice. And if you mouse over the |>., it tells you exactly what it does and why.