From feedb539cd3d41d4073d43b45fc27815b878d4d9 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 21 Nov 2020 00:16:26 +0100
Subject: [PATCH] chore: import orphaned files in `Lean`

---
 src/Lean.lean      |  2 ++
 src/Lean/Data.lean | 20 ++++++++++++++++++++
 2 files changed, 22 insertions(+)
 create mode 100644 src/Lean/Data.lean

diff --git a/src/Lean.lean b/src/Lean.lean
index a840d18df3..8af268eb56 100644
--- a/src/Lean.lean
+++ b/src/Lean.lean
@@ -3,6 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.Data
 import Lean.Compiler
 import Lean.Environment
 import Lean.Modifiers
@@ -25,3 +26,4 @@ import Lean.Delaborator
 import Lean.PrettyPrinter
 import Lean.CoreM
 import Lean.InternalExceptionId
+import Lean.Server
diff --git a/src/Lean/Data.lean b/src/Lean/Data.lean
new file mode 100644
index 0000000000..eba3145383
--- /dev/null
+++ b/src/Lean/Data.lean
@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/
+import Lean.Data.Format
+import Lean.Data.FormatMacro
+import Lean.Data.Json
+import Lean.Data.JsonRpc
+import Lean.Data.KVMap
+import Lean.Data.LBool
+import Lean.Data.LOption
+import Lean.Data.Lsp
+import Lean.Data.Name
+import Lean.Data.Occurrences
+import Lean.Data.OpenDecl
+import Lean.Data.Options
+import Lean.Data.Position
+import Lean.Data.SMap
+import Lean.Data.Trie