diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean index ec38972a1e..57b229b4b3 100644 --- a/src/Lean/Meta/DiscrTree.lean +++ b/src/Lean/Meta/DiscrTree.lean @@ -96,13 +96,14 @@ where if args.isEmpty then return f else - let mut r := f + let mut r := m!"" for arg in args do - r := r ++ m!" {arg}" + r := r ++ Format.line ++ arg + r := f ++ .nest 2 r if parenIfNonAtomic then - return m!"({r})" + return .paren r else - return r + return .group r go (parenIfNonAtomic := true) : StateRefT (List Key) CoreM MessageData := do let some key ← next? | return .nil