max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: import orphaned files in Lean

Browse source
This commit is contained in:
Sebastian Ullrich 2020-11-21 00:16:26 +01:00
parent a6f8ff94ca
commit feedb539cd
2 changed files with 22 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean.lean
View file

@ -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

20
src/Lean/Data.lean Normal file
View file

@ -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