chore: reorganization in Array/Basic (#5400)

Getting started on `Array`.
leanprover · Sep 20, 2024 · 152ca85 · 152ca85
1 parent 0ecf2a0
commit 152ca85
Show file tree

Hide file tree

Showing 5 changed files with 252 additions and 245 deletions.
diff --git a/src/Init/Data/Array.lean b/src/Init/Data/Array.lean
@@ -15,3 +15,4 @@ import Init.Data.Array.BasicAux
 import Init.Data.Array.Lemmas
 import Init.Data.Array.TakeDrop
 import Init.Data.Array.Bootstrap
+import Init.Data.Array.GetLit