simplify

Author: nomeata

src/Lean/Elab/BindersUtil.lean

@@ -48,14 +48,14 @@ open TSyntax.Compat in
 /--
   Expand a match alternative such as `| 0 | 1 => rhs` to an array containing `| 0 => rhs` and `| 1 => rhs`.
 -/
-def expandMatchAlt (stx : TSyntax ``matchAlt) : MacroM (Array (TSyntax ``matchAlt)) :=
+def expandMatchAlt (stx : TSyntax ``matchAlt) : Array (TSyntax ``matchAlt) :=
   -- Not using syntax quotations here to keep source location
   -- of the pattern sequence (`$term,*`) intact
   let patss := stx.raw[1].getSepArgs
   if patss.size ≤ 1 then
-    return #[stx]
+    #[stx]
   else
-    return patss.map fun pats => stx.raw.setArg 1 (mkNullNode #[pats])
+    patss.map fun pats => stx.raw.setArg 1 (mkNullNode #[pats])
 
 def shouldExpandMatchAlt : TSyntax ``matchAlt → Bool
   | `(matchAltExpr| | $[$patss,*]|* => $_) => patss.size > 1
@@ -65,7 +65,7 @@ def expandMatchAlts? (stx : Syntax) : MacroM (Option Syntax) := do
   match stx with
   | `(match $[$gen]? $[$motive]? $discrs,* with $alts:matchAlt*) =>
     if alts.any shouldExpandMatchAlt then
-      let alts ← alts.foldlM (init := #[]) fun alts alt => return alts ++ (← expandMatchAlt alt)
+      let alts ← alts.foldlM (init := #[]) fun alts alt => return alts ++ (expandMatchAlt alt)
       `(match $[$gen]? $[$motive]? $discrs,* with $alts:matchAlt*)
     else
       return none

src/Lean/Elab/Do.lean

@@ -1621,7 +1621,7 @@ mutual
     let optMotive := doMatch[2]
     let discrs    := doMatch[3]
     let matchAlts := doMatch[5][0].getArgs -- Array of `doMatchAlt`
-    let matchAlts ← matchAlts.foldlM (init := #[]) fun result matchAlt => return result ++ (← liftMacroM <| expandMatchAlt matchAlt)
+    let matchAlts ← matchAlts.foldlM (init := #[]) fun result matchAlt => return result ++ (expandMatchAlt matchAlt)
     let alts ←  matchAlts.mapM fun matchAlt => do
       let patterns := matchAlt[1][0]
       let vars ← getPatternsVarsEx patterns.getSepArgs