max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: ppTactic

Browse source
This commit is contained in:
Sebastian Ullrich 2022-07-03 19:00:13 +02:00
parent 5e46c0865e
commit 146aefd085
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/PrettyPrinter.lean
View file

@ -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