diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index e40718bd11..3ea4be7f16 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -9,6 +9,7 @@ import Lean.Class
 import Lean.ReducibilityAttrs
 import Lean.Util.Trace
 import Lean.Util.RecDepth
+import Lean.Util.PPExt
 import Lean.Compiler.InlineAttrs
 import Lean.Meta.Exception
 import Lean.Meta.TransparencyMode
@@ -958,6 +959,16 @@ def dependsOn (e : Expr) (fvarId : FVarId) : m Bool := liftMetaM do
 mctx ← getMCtx;
 pure $ mctx.exprDependsOn e fvarId
 
+def ppExprImp (e : Expr) : MetaM Format := do
+env  ← getEnv;
+mctx ← getMCtx;
+lctx ← getLCtx;
+opts ← getOptions;
+pure $ Lean.ppExpr env mctx lctx opts e
+
+def ppExpr (e : Expr) : m Format :=
+liftMetaM $ ppExprImp e
+
 end Methods
 end Meta