chore: reorganization in Array/Basic (#5400)

Getting started on `Array`.
leanprover · Sep 20, 2024 · 3541cb7 · 3541cb7
1 parent c3f384d
commit 3541cb7
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