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