From decab1ea57bf506b8275f07d1979389a0e92a030 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 25 Jun 2020 11:20:47 -0700
Subject: [PATCH] fix: missing import

---
 src/Init/Data.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Init/Data.lean b/src/Init/Data.lean
index edfd8ed374..fb7d7189cd 100644
--- a/src/Init/Data.lean
+++ b/src/Init/Data.lean
@@ -11,6 +11,7 @@ import Init.Data.String
 import Init.Data.List
 import Init.Data.Int
 import Init.Data.Array
+import Init.Data.PersistentArray
 import Init.Data.ByteArray
 import Init.Data.FloatArray
 import Init.Data.Fin