From 79afaa74219317510f211c2b0b90eb85def2a17d Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Fri, 24 Feb 2017 20:17:19 +0100
Subject: [PATCH] feat(library/init/meta/tactic): add timetac combinator

---
 library/init/meta/tactic.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 52df5bec85..3c00e05c5f 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -196,6 +196,9 @@ do fmt ← pp a,
 meta def trace_call_stack : tactic unit :=
 take state, _root_.trace_call_stack (success () state)
 
+meta def timetac {α : Type u} (desc : string) (t : tactic α) : tactic α :=
+λ s, timeit desc (t s)
+
 meta def trace_state : tactic unit :=
 do s ← read,
    trace $ to_fmt s