feat(init/util): tactic.trace-like trace_val function

Calling it `trace` and removing the old `trace` function does bad things with overloading

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 ()