chore(library/init/lean/compiler): missing prelude

2019-05-03 09:11:12 -07:00 · 2019-05-03 09:11:12 -07:00 · 4cafd19f72
commit 4cafd19f72
parent c77970a00f
3 changed files with 3 additions and 0 deletions
--- a/library/init/lean/compiler/elimdead.lean
+++ b/library/init/lean/compiler/elimdead.lean
@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import init.lean.compiler.ir

 namespace Lean
--- a/library/init/lean/compiler/pushproj.lean
+++ b/library/init/lean/compiler/pushproj.lean
@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import init.lean.compiler.ir

 namespace Lean
--- a/library/init/lean/compiler/simpcase.lean
+++ b/library/init/lean/compiler/simpcase.lean
@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import init.lean.compiler.ir

 namespace Lean