From 146aefd085bbe68698b9df7dc0855dfa72a9000a Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sun, 3 Jul 2022 19:00:13 +0200
Subject: [PATCH] feat: ppTactic

---
 src/Lean/PrettyPrinter.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean
index e31f729b8b..fa8a42e37b 100644
--- a/src/Lean/PrettyPrinter.lean
+++ b/src/Lean/PrettyPrinter.lean
@@ -50,6 +50,9 @@ def ppConst (e : Expr) : MetaM Format := do
 def ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : IO Format :=
   Prod.fst <$> ((ppExpr e).run' { lctx := lctx } { mctx := mctx }).toIO { options := opts, fileName := "<PrettyPrinter>", fileMap := default } { env := env }
 
+def ppTactic (stx : Syntax) : CoreM Format :=
+  parenthesizeTactic stx >>= formatTactic
+
 def ppCommand (stx : Syntax) : CoreM Format :=
   parenthesizeCommand stx >>= formatCommand