From f28def6c5e0ffc80594cd9dfdd672f1e7e38feec Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 10 Sep 2020 17:27:14 -0700
Subject: [PATCH] feat: add `Meta.ppExpr`

---
 src/Lean/Meta/Basic.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)

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