doc: fix docstring of List.span (#3707)

see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/docstring.20of.20.60List.2Espan.60.20is.20wrong
2024-03-18 19:26:47 +09:00 · 2024-03-18 19:26:47 +09:00 · 7abc1fdaac
commit 7abc1fdaac
parent 2d18eff544
1 changed files with 1 additions and 1 deletions
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@ -458,7 +458,7 @@ contains the longest initial segment for which `p` returns true
 and the second part is everything else.

 * `span (· > 5) [6, 8, 9, 5, 2, 9] = ([6, 8, 9], [5, 2, 9])`
-* `span (· > 10) [6, 8, 9, 5, 2, 9] = ([6, 8, 9, 5, 2, 9], [])`
+* `span (· > 10) [6, 8, 9, 5, 2, 9] = ([], [6, 8, 9, 5, 2, 9])`
 -/
@[inline] def span (p : α → Bool) (as : List α) : List α × List α :=
  loop as []