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