diff --git a/library/init/util.lean b/library/init/util.lean
index f7762c8f9a..ad360651c7 100644
--- a/library/init/util.lean
+++ b/library/init/util.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.string.basic
+import init.meta.format
 universes u
 
 /- This function has a native implementation that tracks time. -/
@@ -15,6 +15,9 @@ f ()
 def trace {α : Type u} (s : string) (f : thunk α) : α :=
 f ()
 
+meta def trace_val {α : Type u} [has_to_format α] (f : α) : α :=
+trace (to_string (to_fmt f)) f
+
 /- This function has a native implementation that shows the VM call stack. -/
 def trace_call_stack {α : Type u} (f : thunk α) : α :=
 f ()