From 7c393a1b3f82408e0d5f07b80d4b351f7fc1ab9a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 10 Nov 2020 14:06:11 -0800
Subject: [PATCH] chore: cleanup

---
 tmp/PreludeNew.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/tmp/PreludeNew.lean b/tmp/PreludeNew.lean
index 959619acbb..2d53ec9704 100644
--- a/tmp/PreludeNew.lean
+++ b/tmp/PreludeNew.lean
@@ -1119,7 +1119,7 @@ instance (σ : Type u) (m : Type u → Type v) [MonadStateOf σ m] : MonadState
 @[inline] def modify {σ : Type u} {m : Type u → Type v} [MonadState σ m] (f : σ → σ) : m PUnit :=
   modifyGet fun s => (PUnit.unit, f s)
 
-@[inline] def getModify {σ : Type u} {m : Type u → Type v} [MonadState σ m] [Monad m] (f : σ → σ) : m σ := do
+@[inline] def getModify {σ : Type u} {m : Type u → Type v} [MonadState σ m] [Monad m] (f : σ → σ) : m σ :=
   modifyGet fun s => (s, f s)
 
 -- NOTE: The Ordering of the following two instances determines that the top-most `StateT` Monad layer
@@ -1555,7 +1555,7 @@ def addMacroScope (mainModule : Name) (n : Name) (scp : MacroScope) : Name :=
   match n.hasMacroScopes with
   | true =>
     let view := extractMacroScopes n
-    match view.mainModule == mainModule with
+    match beq view.mainModule mainModule with
     | true  => mkNameNum n scp
     | false =>
       { view with
@@ -1648,8 +1648,8 @@ def expandMacroNotAvailable? (stx : Syntax) : MacroM (Option Syntax) :=
 def mkMacroEnvSimple : MacroEnv :=
   mkMacroEnv expandMacroNotAvailable?
 
-unsafe def expandMacro?Imp (stx : Syntax) : MacroM (Option Syntax) := do
-  let ctx ← read
+unsafe def expandMacro?Imp (stx : Syntax) : MacroM (Option Syntax) :=
+  bind read fun ctx =>
   let f : Syntax → MacroM (Option Syntax) := unsafeCast (ctx.macroEnv)
   f stx