diff --git a/library/init/meta/level.lean b/library/init/meta/level.lean
index 8b3a4f0dfc..c67c5e9c8e 100644
--- a/library/init/meta/level.lean
+++ b/library/init/meta/level.lean
@@ -7,7 +7,7 @@ prelude
 import init.meta.name init.meta.format
 
 /- Reflect a C++ level object. The VM replaces it with the C++ implementation. -/
-inductive level
+meta inductive level
 | zero   : level
 | succ   : level → level
 | max    : level → level → level
@@ -15,7 +15,7 @@ inductive level
 | param  : name → level
 | mvar   : name → level
 
-instance : inhabited level :=
+meta instance : inhabited level :=
 ⟨level.zero⟩
 
 /- TODO(Leo): provide a definition in Lean. -/