From 2b0ed751bdabaef77766d5ebd3f9ea630d84b7ca Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Mon, 8 Jul 2024 09:57:50 +0200
Subject: [PATCH] fix: unorphan modules in Init (#4680)

---
 src/Init/Data.lean       | 1 +
 src/Init/Data/Array.lean | 1 +
 2 files changed, 2 insertions(+)

diff --git a/src/Init/Data.lean b/src/Init/Data.lean
index f6da558757..2f1a41173e 100644
--- a/src/Init/Data.lean
+++ b/src/Init/Data.lean
@@ -35,3 +35,4 @@ import Init.Data.Queue
 import Init.Data.Channel
 import Init.Data.Cast
 import Init.Data.Sum
+import Init.Data.BEq
diff --git a/src/Init/Data/Array.lean b/src/Init/Data/Array.lean
index 2fbb0cb3e6..d74a7ba067 100644
--- a/src/Init/Data/Array.lean
+++ b/src/Init/Data/Array.lean
@@ -13,3 +13,4 @@ import Init.Data.Array.Mem
 import Init.Data.Array.Attach
 import Init.Data.Array.BasicAux
 import Init.Data.Array.Lemmas
+import Init.Data.Array.TakeDrop