diff --git a/library/init/default.lean b/library/init/default.lean
index 17c8c61d58..7a465a566c 100644
--- a/library/init/default.lean
+++ b/library/init/default.lean
@@ -5,8 +5,10 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.datatypes init.reserved_notation init.logic
-import init.relation init.wf init.nat init.wf_k init.prod
+import init.relation init.nat init.prod
 import init.bool init.num init.sigma init.measurable init.setoid init.quot
 import init.funext init.function init.subtype init.classical init.simplifier
 import init.monad init.fin init.list init.char init.string init.to_string init.timeit
 import init.unsigned
+import init.meta
+import init.wf init.wf_k
diff --git a/library/meta/base_tactic.lean b/library/init/meta/base_tactic.lean
similarity index 98%
rename from library/meta/base_tactic.lean
rename to library/init/meta/base_tactic.lean
index b69d9add27..49b970130b 100644
--- a/library/meta/base_tactic.lean
+++ b/library/init/meta/base_tactic.lean
@@ -3,7 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import meta.format
+prelude
+import init.monad init.meta.format
 /-
 Remark: we use a thunk that produces a format object as the exception information.
 Motivation: the formatting object may be big.
diff --git a/library/meta/cmp_result.lean b/library/init/meta/cmp_result.lean
similarity index 97%
rename from library/meta/cmp_result.lean
rename to library/init/meta/cmp_result.lean
index bfc466def5..8a33726441 100644
--- a/library/meta/cmp_result.lean
+++ b/library/init/meta/cmp_result.lean
@@ -3,6 +3,9 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
+import init.to_string init.prod
+
 inductive cmp_result :=
 | lt | eq | gt
 
diff --git a/library/meta/default.lean b/library/init/meta/default.lean
similarity index 53%
rename from library/meta/default.lean
rename to library/init/meta/default.lean
index e2838b27c4..99a8c777fe 100644
--- a/library/meta/default.lean
+++ b/library/init/meta/default.lean
@@ -3,5 +3,6 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import meta.name meta.options meta.format meta.rb_map
-import meta.level meta.expr
+prelude
+import init.meta.name init.meta.options init.meta.format init.meta.rb_map
+import init.meta.level init.meta.expr init.meta.base_tactic
diff --git a/library/meta/expr.lean b/library/init/meta/expr.lean
similarity index 98%
rename from library/meta/expr.lean
rename to library/init/meta/expr.lean
index f28b75b801..dd7a011533 100644
--- a/library/meta/expr.lean
+++ b/library/init/meta/expr.lean
@@ -3,7 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import meta.level
+prelude
+import init.meta.level
 
 inductive binder_info :=
 | default | implicit | strict_implicit | inst_implicit | other
diff --git a/library/meta/format.lean b/library/init/meta/format.lean
similarity index 90%
rename from library/meta/format.lean
rename to library/init/meta/format.lean
index 0cd8c4f753..64febdd2fe 100644
--- a/library/meta/format.lean
+++ b/library/init/meta/format.lean
@@ -3,7 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import system.IO meta.options
+prelude
+import init.meta.options
 
 inductive format.color :=
 | red | green | orange | blue | pink | cyan | grey
@@ -19,12 +20,8 @@ meta_constant format.of_string   : string → format
 meta_constant format.of_nat      : nat → format
 meta_constant format.flatten     : format → format
 meta_constant format.to_string   : format → options → string
-meta_constant format.print_using : format → options → IO unit
 meta_constant format.of_options  : options → format
 
-meta_definition format.print (fmt : format) : IO unit :=
-format.print_using fmt options.mk
-
 meta_definition format_has_add [instance] : has_add format :=
 has_add.mk format.compose
 
@@ -37,12 +34,6 @@ structure has_to_format [class] (A : Type) :=
 meta_definition to_fmt {A : Type} [has_to_format A] : A → format :=
 has_to_format.to_format
 
-meta_definition pp_using {A : Type} [has_to_format A] (a : A) (o : options) : IO unit :=
-format.print_using (to_fmt a) o
-
-meta_definition pp {A : Type} [has_to_format A] (a : A) : IO unit :=
-format.print (to_fmt a)
-
 namespace format
 attribute [coercion] of_string of_nat
 end format
diff --git a/library/meta/level.lean b/library/init/meta/level.lean
similarity index 98%
rename from library/meta/level.lean
rename to library/init/meta/level.lean
index 2444e4f699..f5a8ef1744 100644
--- a/library/meta/level.lean
+++ b/library/init/meta/level.lean
@@ -3,7 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import meta.name meta.format
+prelude
+import init.meta.name init.meta.format
 
 /- Reflect a C++ level object. The VM replaces it with the C++ implementation. -/
 inductive level :=
diff --git a/library/meta/name.lean b/library/init/meta/name.lean
similarity index 97%
rename from library/meta/name.lean
rename to library/init/meta/name.lean
index ca3589b322..d97d626e2a 100644
--- a/library/meta/name.lean
+++ b/library/init/meta/name.lean
@@ -3,7 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import meta.cmp_result
+prelude
+import init.meta.cmp_result
 
 /- Reflect a C++ name object. The VM replaces it with the C++ implementation. -/
 inductive name :=
diff --git a/library/meta/options.lean b/library/init/meta/options.lean
similarity index 97%
rename from library/meta/options.lean
rename to library/init/meta/options.lean
index 2a756ca22c..80b7a2ea12 100644
--- a/library/meta/options.lean
+++ b/library/init/meta/options.lean
@@ -3,7 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import meta.name
+prelude
+import init.meta.name
 
 meta_constant options                  : Type₁
 meta_constant options.size             : options → nat
diff --git a/library/meta/rb_map.lean b/library/init/meta/rb_map.lean
similarity index 97%
rename from library/meta/rb_map.lean
rename to library/init/meta/rb_map.lean
index b7cec35437..4af5c18cae 100644
--- a/library/meta/rb_map.lean
+++ b/library/init/meta/rb_map.lean
@@ -3,7 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import meta.cmp_result meta.name meta.format
+prelude
+import init.meta.cmp_result init.meta.name init.meta.format
 
 meta_constant rb_map.{l₁ l₂} : Type.{l₁} → Type.{l₂} → Type.{max l₁ l₂ 1}
 
diff --git a/library/system/IO.lean b/library/system/IO.lean
index 8ce8090adb..c1b4616772 100644
--- a/library/system/IO.lean
+++ b/library/system/IO.lean
@@ -12,3 +12,14 @@ attribute [instance] functorIO monadIO
 constant put_str : string → IO unit
 constant put_nat : nat → IO unit
 constant get_line : IO string
+
+meta_constant format.print_using : format → options → IO unit
+
+meta_definition format.print (fmt : format) : IO unit :=
+format.print_using fmt options.mk
+
+meta_definition pp_using {A : Type} [has_to_format A] (a : A) (o : options) : IO unit :=
+format.print_using (to_fmt a) o
+
+meta_definition pp {A : Type} [has_to_format A] (a : A) : IO unit :=
+format.print (to_fmt a)
diff --git a/tests/lean/run/base_tac1.lean b/tests/lean/run/base_tac1.lean
index 004348cd19..26be1489ff 100644
--- a/tests/lean/run/base_tac1.lean
+++ b/tests/lean/run/base_tac1.lean
@@ -1,4 +1,3 @@
-import meta.base_tactic
 open tactic
 
 meta_definition tac [reducible] := base_tactic string
diff --git a/tests/lean/run/format.lean b/tests/lean/run/format.lean
index 742ddd49e0..71fc027500 100644
--- a/tests/lean/run/format.lean
+++ b/tests/lean/run/format.lean
@@ -1,4 +1,4 @@
-import meta
+import system.IO
 open list
 
 vm_eval pp ([["aaa", "bbb", "ccc", "dddd", "eeeeee", "ffffff"], ["aaa", "bbb", "ccc", "dddd", "eeeeee", "ffffff"],
diff --git a/tests/lean/run/meta_expr1.lean b/tests/lean/run/meta_expr1.lean
index 66e2ad8529..d416105556 100644
--- a/tests/lean/run/meta_expr1.lean
+++ b/tests/lean/run/meta_expr1.lean
@@ -1,4 +1,3 @@
-import meta
 open unsigned list
 
 meta_definition e1 := expr.app (expr.app (expr.const "f" []) (expr.mk_var 1)) (expr.const "a" [])
diff --git a/tests/lean/run/meta_level1.lean b/tests/lean/run/meta_level1.lean
index da1395958c..1cc309a0ef 100644
--- a/tests/lean/run/meta_level1.lean
+++ b/tests/lean/run/meta_level1.lean
@@ -1,4 +1,4 @@
-import meta
+import system.IO
 
 vm_eval do pp (level.max (level.succ level.zero) (level.param "foo")), put_str "\n"
 
diff --git a/tests/lean/run/opt1.lean b/tests/lean/run/opt1.lean
index 23fef91d36..4ac7e2c308 100644
--- a/tests/lean/run/opt1.lean
+++ b/tests/lean/run/opt1.lean
@@ -1,5 +1,3 @@
-import meta
-
 vm_eval options.get_string options.mk "opt1" "<empty>"
 vm_eval options.get_string (options.set_string options.mk "opt1" "val1") "opt1" "<empty>"
 vm_eval if (options.mk = options.mk) then bool.tt else bool.ff
diff --git a/tests/lean/run/rb_map1.lean b/tests/lean/run/rb_map1.lean
index e34b6a8c8d..a95d2109a5 100644
--- a/tests/lean/run/rb_map1.lean
+++ b/tests/lean/run/rb_map1.lean
@@ -1,4 +1,4 @@
-import meta
+import system.IO
 
 section
 open nat_map