feat: port List.traverse (#398)

Std/Data/List/Basic.lean

@@ -1628,4 +1628,12 @@ Example: if `f : Nat → list Nat → β`, `List.mapWithComplement f [1, 2, 3]`
 def mapWithComplement {α β} (f : α → List α → β) : List α → List β :=
   mapWithPrefixSuffix fun pref a suff => f a (pref ++ suff)
 
+/--
+Map each element of a `List` to an action, evaluate these actions in order,
+and collect the results.
+-/
+protected def traverse [Applicative F] (f : α → F β) : List α → F (List β)
+  | [] => pure []
+  | x :: xs => List.cons <$> f x <*> List.traverse f xs
+
 end List