Hacker News new | ask | show | jobs
by ykonstant 1020 days ago
Surely you can define such notation, but why? The following is just as clear and concise, and does not rely on any extensions:

    (. * 2) <$> [1,2,3]
For example:

    def byTwo (inputList : List Nat) :=
      (. * 2) <$> inputList

    #eval byTwo [1, 2, 3]
    -- [2, 4, 6]
2 comments
2pEXgD0fZ5cF 1020 days ago
> but why?

Why not? I was curious, Haskell is the functional language I know. Lean is the language I do not know.

Since Lean leans even heavier towards mathematics, set builder style notation seems like a natural fit. Now whether or not such notation is actually needed or worth it, that is a whole different question.

link
kmill 1020 days ago
That's not exactly clear to mathematicians, who tend to complain about the "ascii art operators".

I think you'll usually see

    def byTwo (inputList : List.Nat) := inputList.map (. \* 2)
rather than using `<$>`. There's also `inputList |>.map (. * 2)`, but I haven't seen it in any mathlib theory code yet, just Lean core or in metaprogramming.
link