feat(library/init/meta/tactic): add timetac combinator

This commit is contained in:
Gabriel Ebner 2017-02-24 20:17:19 +01:00
parent b5276a1c6f
commit 79afaa7421

View file

@ -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