diff --git a/src/Init/Data/Array.lean b/src/Init/Data/Array.lean index daaced8f1c..d26bc11b7a 100644 --- a/src/Init/Data/Array.lean +++ b/src/Init/Data/Array.lean @@ -9,3 +9,4 @@ import Init.Data.Array.QSort import Init.Data.Array.BinSearch import Init.Data.Array.InsertionSort import Init.Data.Array.DecidableEq +import Init.Data.Array.Mem