chained dot notation

Stream: lean4

[Juan Pablo Romero]

Hi, curious if there's a way to write this expression:

([1, 2].map (. + 1)).map toString

in this style:

[1, 2]
  .map (. + 1)
  .map toString

(to mimic chained dot notation in OO languages)

[Henrik Böving]

Not exactly but very close:

#eval #[1, 2]
        |>.map (. + 1)
        |>.map toString

[Henrik Böving]

In general after a some expression |> you can always use .foo (note that there must not be a blank before the dot here, if there is it has a completely different semantic) to mimick (some epxression).foo

[Juan Pablo Romero]

ah, pretty cool!

[Henrik Böving]

If you want to know what an alone standing .foo would mean, basically if Lean expects a function that results in a type a at this point it will look up the name foo in namespace a so writing e.g.

def foo : Array Nat := #[1,2,3].map (.add 12)

will make Lean use Nat.add here, you can also use this in pattern matching:

def test : Nat → Nat
  | .zero => 0
  | .succ n => n

[Juan Pablo Romero]

yes, I love that feature