Skip to content

Commit

Permalink
chore: join → flatten in docstring (#6040)
Browse files Browse the repository at this point in the history
Update the docstring of `List.flatten`.
  • Loading branch information
vihdzp authored Nov 15, 2024
1 parent a074bd9 commit 7e6363d
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Init/Data/List/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 α
Expand Down

0 comments on commit 7e6363d

Please sign in to comment.