5 ms·
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 ex
by ykonstant 3y 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]
- 2pEXgD0fZ5cF 3y 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.
- kmill 3y agoThat'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.