From ac8d9e254e4639bb03891232ddbe5d47ae8163cd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 4 Dec 2021 22:31:10 +0100 Subject: [PATCH] feat: parenthesize in the pretty printer --- DocGen4/Process.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 4c72fdf..9e5924e 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -72,8 +72,9 @@ structure Module where members : Array DocInfo deriving Inhabited -def prettyPrintTerm (expr : Expr) : MetaM Syntax := - delab Name.anonymous [] expr +def prettyPrintTerm (expr : Expr) : MetaM Syntax := do + let term ← delab Name.anonymous [] expr + parenthesizeTerm term def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do let env ← getEnv