From 94804358fafb264c515b54410ffdc74fc810d17b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 16 Mar 2020 14:28:42 -0700
Subject: [PATCH] chore: better trace message

---
 src/Init/Lean/Elab/Definition.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Lean/Elab/Definition.lean b/src/Init/Lean/Elab/Definition.lean
index 111a4b1ab9..d99c6504d0 100644
--- a/src/Init/Lean/Elab/Definition.lean
+++ b/src/Init/Lean/Elab/Definition.lean
@@ -107,7 +107,7 @@ else withUsedWhen ref vars xs val type view.kind.isDefOrAbbrevOrOpaque $ fun var
     pure (type, val)
   };
   let (type, val) := shareCommonTypeVal.run;
-  Term.trace `Elab.definition.body ref $ fun _ => val;
+  Term.trace `Elab.definition.body ref $ fun _ => declName ++ " : " ++ type ++ " :=" ++ Format.line ++ val;
   let usedParams : CollectLevelParams.State := {};
   let usedParams  := collectLevelParams usedParams type;
   let usedParams  := collectLevelParams usedParams val;