Skip to content

Commit

Permalink
doc: improve List.toArray doc-string (leanprover#6962)
Browse files Browse the repository at this point in the history
This PR improves the doc-string for `List.toArray`.

Thanks to @jt0202 for pointing this out.
  • Loading branch information
kim-em authored and luisacicolini committed Feb 25, 2025
1 parent ebaea41 commit 74478d4
Showing 1 changed file with 7 additions and 1 deletion.
8 changes: 7 additions & 1 deletion src/Init/Prelude.lean
Original file line number Diff line number Diff line change
Expand Up @@ -2612,7 +2612,13 @@ structure Array (α : Type u) where
attribute [extern "lean_array_to_list"] Array.toList
attribute [extern "lean_array_mk"] Array.mk

@[inherit_doc Array.mk, match_pattern]
/--
Converts a `List α` into an `Array α`. (This is preferred over the synonym `Array.mk`.)
At runtime, this constructor is implemented by `List.toArrayImpl` and is O(n) in the length of the
list.
-/
@[match_pattern]
abbrev List.toArray (xs : List α) : Array α := .mk xs

/-- Construct a new empty array with initial capacity `c`. -/
Expand Down

0 comments on commit 74478d4

Please sign in to comment.