From 4483e53de06a92aac46aba36cdf4f2da4875b95d Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 11 Apr 2017 13:30:20 +0200
Subject: [PATCH] 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 | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

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