From a69178ea9f43b8b24924d29d7a6532ed32460f76 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 18 Aug 2020 13:24:32 -0700
Subject: [PATCH] feat: add `MonadTracer` instance

---
 src/Lean/Util/Trace.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean
index 87e9537c2b..20bfd3b91d 100644
--- a/src/Lean/Util/Trace.lean
+++ b/src/Lean/Util/Trace.lean
@@ -15,6 +15,11 @@ class MonadTracer (m : Type → Type u) :=
 (trace  : Name → (Unit → MessageData) → m PUnit)
 (traceM : Name → m MessageData → m PUnit)
 
+instance ReaderT.monadTracer (ρ : Type) (m : Type → Type) [MonadTracer m] : MonadTracer (ReaderT ρ m) :=
+{ traceCtx := fun α n x ctx => MonadTracer.traceCtx n (x ctx),
+  trace    := fun n x _     => MonadTracer.trace n x,
+  traceM   := fun n x ctx   => MonadTracer.traceM n (x ctx) }
+
 class MonadTracerAdapter (m : Type → Type) :=
 (isTracingEnabledFor : Name → m Bool)
 (addContext          : MessageData → m MessageData)