|
|
|
|
|
|
by kmill
1015 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. |
|
|