docs: RArray is now universe-polymorphic

This PR adjusts the RArray docstring to the new realty from #8014.
2026-03-23 13:24:11 +00:00 · 2025-04-18 09:28:20 +02:00
1 changed files with 0 additions and 3 deletions
--- a/src/Init/Data/RArray.lean
+++ b/src/Init/Data/RArray.lean
@@ -22,9 +22,6 @@ tree implementing `Nat → α`.

 See `RArray.ofFn` and `RArray.ofArray` in module `Lean.Data.RArray` for functions that construct an
 `RArray`.
-
-It is not universe-polymorphic. ; smaller proof objects and no complication with the `ToExpr` type
-class.
 -/
 inductive RArray (α : Type u) : Type u where
  | leaf : α → RArray α