From e6343497a730fe32e9c0b4cc4fd11a15ac4be711 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 18 Apr 2025 11:23:05 +0200 Subject: [PATCH] doc: RArray is now universe-polymorphic (#8018) This PR adjusts the RArray docstring to the new reality from #8014. --- src/Init/Data/RArray.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/Init/Data/RArray.lean b/src/Init/Data/RArray.lean index ece98d5377..0b423d8fdd 100644 --- 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 α