max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add MonadTracer instance

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-18 13:24:32 -07:00
parent b142c608fe
commit a69178ea9f
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Util/Trace.lean
View file

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