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 α