From 028531ba9bcff44753b0789e6e48e08b32bd5935 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 2 Dec 2019 11:41:44 -0800
Subject: [PATCH] chore: `M` => `SynthM`

---
 src/Init/Lean/Meta/SynthInstance.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Init/Lean/Meta/SynthInstance.lean b/src/Init/Lean/Meta/SynthInstance.lean
index 47022f10de..09bd907077 100644
--- a/src/Init/Lean/Meta/SynthInstance.lean
+++ b/src/Init/Lean/Meta/SynthInstance.lean
@@ -62,26 +62,26 @@ structure State extends Meta.State :=
 (tableKeys      : DiscrTree Key               := {})
 (tableEntries   : PersistentArray TableEntry  := {})
 
-abbrev M := ReaderT Context (EStateM Exception State)
+abbrev SynthM := ReaderT Context (EStateM Exception State)
 
-@[inline] private def getTraceState : M TraceState :=
+@[inline] private def getTraceState : SynthM TraceState :=
 do s ← get; pure s.traceState
 
-@[inline] private def getOptions : M Options :=
+@[inline] private def getOptions : SynthM Options :=
 do ctx ← read; pure ctx.config.opts
 
-instance tracer : SimpleMonadTracerAdapter M :=
+instance tracer : SimpleMonadTracerAdapter SynthM :=
 { getOptions       := getOptions,
   getTraceState    := getTraceState,
   modifyTraceState := fun f => modify $ fun s => { traceState := f s.traceState, .. s } }
 
-@[inline] def trace (cls : Name) (mctx : MetavarContext) (msg : Unit → MessageData) : M Unit :=
+@[inline] def trace (cls : Name) (mctx : MetavarContext) (msg : Unit → MessageData) : SynthM Unit :=
 whenM (MonadTracerAdapter.isTracingEnabledFor cls) $ do
   ctx ← read;
   s   ← get;
   MonadTracerAdapter.addTrace cls (MessageData.context s.env mctx ctx.lctx (msg ()))
 
-@[inline] def runMetaM {α} (x : MetaM α) : M α :=
+@[inline] def runMetaM {α} (x : MetaM α) : SynthM α :=
 fun ctx => adaptState (fun (s : State) => (s.toState, s)) (fun s' s => { toState := s', .. s }) (x ctx.toContext)
 
 def main (type : Expr) : MetaM (Option Expr) :=