diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 97bf91126e..d5622cc9cf 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -12,6 +12,7 @@ import Lean.Util.RecDepth
 import Lean.Util.Closure
 import Lean.Compiler.InlineAttrs
 import Lean.Meta.Exception
+import Lean.Meta.TransparencyMode
 import Lean.Meta.DiscrTreeTypes
 import Lean.Eval
 import Lean.CoreM
@@ -29,35 +30,6 @@ They are packed into the MetaM monad.
 namespace Lean
 namespace Meta
 
-inductive TransparencyMode
-| all | default | reducible
-
-namespace TransparencyMode
-instance : Inhabited TransparencyMode := ⟨TransparencyMode.default⟩
-
-def beq : TransparencyMode → TransparencyMode → Bool
-| all,       all       => true
-| default,   default   => true
-| reducible, reducible => true
-| _,         _         => false
-
-instance : HasBeq TransparencyMode := ⟨beq⟩
-
-def hash : TransparencyMode → USize
-| all       => 7
-| default   => 11
-| reducible => 13
-
-instance : Hashable TransparencyMode := ⟨hash⟩
-
-def lt : TransparencyMode → TransparencyMode → Bool
-| reducible, default => true
-| reducible, all     => true
-| default,   all     => true
-| _,         _       => false
-
-end TransparencyMode
-
 structure Config :=
 (foApprox           : Bool    := false)
 (ctxApprox          : Bool    := false)
diff --git a/src/Lean/Meta/TransparencyMode.lean b/src/Lean/Meta/TransparencyMode.lean
new file mode 100644
index 0000000000..4cc204299c
--- /dev/null
+++ b/src/Lean/Meta/TransparencyMode.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+namespace Lean
+namespace Meta
+
+inductive TransparencyMode
+| all | default | reducible
+
+namespace TransparencyMode
+instance : Inhabited TransparencyMode := ⟨TransparencyMode.default⟩
+
+def beq : TransparencyMode → TransparencyMode → Bool
+| all,       all       => true
+| default,   default   => true
+| reducible, reducible => true
+| _,         _         => false
+
+instance : HasBeq TransparencyMode := ⟨beq⟩
+
+def hash : TransparencyMode → USize
+| all       => 7
+| default   => 11
+| reducible => 13
+
+instance : Hashable TransparencyMode := ⟨hash⟩
+
+def lt : TransparencyMode → TransparencyMode → Bool
+| reducible, default => true
+| reducible, all     => true
+| default,   all     => true
+| _,         _       => false
+
+end TransparencyMode
+
+end Meta
+end Lean