From 1065675b71e193301aa3e86b44ac358bea10c2a1 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Mon, 27 Nov 2023 18:53:19 +1100
Subject: [PATCH] feat: port List.traverse (#398)

---
 Std/Data/List/Basic.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/Std/Data/List/Basic.lean b/Std/Data/List/Basic.lean
index f091297e3f..17bb198c53 100644
--- a/Std/Data/List/Basic.lean
+++ b/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