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

chore: move Message to Lean

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-10 10:58:50 -08:00
parent f8c7d6ca6b
commit a76b104f61
7 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Linter.lean
View file

@ -7,7 +7,7 @@ prelude
import Init.System.IO
import Init.Lean.Attributes
import Init.Lean.Syntax
import Init.Lean.Util.Message
import Init.Lean.Message
namespace Lean

0
src/Init/Lean/Util/Message.lean → src/Init/Lean/Message.lean
View file

2
src/Init/Lean/Meta/Exception.lean
View file

@ -6,7 +6,7 @@ Authors: Leonardo de Moura
prelude
import Init.Lean.Environment
import Init.Lean.MetavarContext
import Init.Lean.Util.Message
import Init.Lean.Message
namespace Lean
namespace Meta

2
src/Init/Lean/Parser/Module.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
prelude
import Init.Lean.Util.Message
import Init.Lean.Message
import Init.Lean.Parser.Command
namespace Lean

2
src/Init/Lean/Parser/Parser.lean
View file

@ -10,7 +10,7 @@ import Init.Lean.Syntax
import Init.Lean.ToExpr
import Init.Lean.Environment
import Init.Lean.Attributes
import Init.Lean.Util.Message
import Init.Lean.Message
import Init.Lean.Parser.Identifier
import Init.Lean.Compiler.InitAttr

2
src/Init/Lean/Util/Sorry.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Lean.Util.Message
import Init.Lean.Message
namespace Lean

2
src/Init/Lean/Util/Trace.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich, Leonardo de Moura
-/
prelude
import Init.Lean.Util.Message
import Init.Lean.Message
universe u
namespace Lean