max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: RArray is now universe-polymorphic (#8018)

Browse source 
This PR adjusts the RArray docstring to the new reality from #8014.
This commit is contained in:
Joachim Breitner 2025-04-18 11:23:05 +02:00 • committed by GitHub
parent 27a7a0a2bd
commit e6343497a7
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/Data/RArray.lean
View file

@ -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 α