From 7e6363dc0528001038b29be942feab23e6c018a7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= <vi.hdz.p@gmail.com>
Date: Fri, 15 Nov 2024 04:11:42 -0600
Subject: [PATCH] =?UTF-8?q?chore:=20join=20=E2=86=92=20flatten=20in=20docs?=
 =?UTF-8?q?tring=20(#6040)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Update the docstring of `List.flatten`.
---
 src/Init/Data/List/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index f0d989e9ecd8..40c2c4a84162 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -551,7 +551,7 @@ theorem reverseAux_eq_append (as bs : List α) : reverseAux as bs = reverseAux a
 /-! ### flatten -/
 
 /--
-`O(|flatten L|)`. `join L` concatenates all the lists in `L` into one list.
+`O(|flatten L|)`. `flatten L` concatenates all the lists in `L` into one list.
 * `flatten [[a], [], [b, c], [d, e, f]] = [a, b, c, d, e, f]`
 -/
 def flatten : List (List α) → List α