From eb1e285e2654de51814fb74bcbad7eb4523cd864 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 19 Jun 2021 11:53:46 +0200
Subject: [PATCH] chore: style

---
 src/Init/Data/Range.lean                      | 2 +-
 src/Lean/Data/Lsp/Ipc.lean                    | 2 +-
 src/Lean/Elab/BuiltinNotation.lean            | 2 +-
 src/Lean/Elab/Command.lean                    | 2 +-
 src/Lean/Elab/Frontend.lean                   | 2 +-
 src/Lean/Elab/Match.lean                      | 6 +++---
 src/Lean/Elab/PreDefinition/MkInhabitant.lean | 8 ++++----
 src/Lean/Elab/PreDefinition/Structural.lean   | 6 +++---
 src/Lean/Elab/Quotation.lean                  | 2 +-
 src/Lean/Elab/Tactic/Injection.lean           | 2 +-
 src/Lean/Elab/Term.lean                       | 2 +-
 src/Lean/Elab/Util.lean                       | 2 +-
 src/Lean/Meta/Tactic/Simp/Rewrite.lean        | 4 ++--
 src/Lean/ReducibilityAttrs.lean               | 2 +-
 src/Lean/Server/FileWorker.lean               | 2 +-
 src/Lean/Server/Requests.lean                 | 2 +-
 src/Lean/Syntax.lean                          | 6 +++---
 src/Std/Data/RBMap.lean                       | 2 +-
 18 files changed, 28 insertions(+), 28 deletions(-)

diff --git a/src/Init/Data/Range.lean b/src/Init/Data/Range.lean
index 0deb8514ec..93e609bff6 100644
--- a/src/Init/Data/Range.lean
+++ b/src/Init/Data/Range.lean
@@ -23,7 +23,7 @@ universes u v
       pure b
     else match i with
      | 0   => pure b
-     | i+1 => match ← f j b with
+     | i+1 => match (← f j b) with
         | ForInStep.done b  => pure b
         | ForInStep.yield b => loop i (j + range.step) b
   loop range.stop range.start init
diff --git a/src/Lean/Data/Lsp/Ipc.lean b/src/Lean/Data/Lsp/Ipc.lean
index 7ca9eff557..570918d48f 100644
--- a/src/Lean/Data/Lsp/Ipc.lean
+++ b/src/Lean/Data/Lsp/Ipc.lean
@@ -54,7 +54,7 @@ partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target :
 : IpcM (List (Notification PublishDiagnosticsParams)) := do
   writeRequest ⟨waitForDiagnosticsId, "textDocument/waitForDiagnostics", WaitForDiagnosticsParams.mk target version⟩
   let rec loop : IpcM (List (Notification PublishDiagnosticsParams)) := do
-    match ←readMessage with
+    match (←readMessage) with
     | Message.response id _ =>
       if id == waitForDiagnosticsId then []
       else loop
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index d99373b123..a37188cad1 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -226,7 +226,7 @@ where
 @[builtinMacro Lean.Parser.Term.paren] def expandParen : Macro
   | `(())           => `(Unit.unit)
   | `(($e : $type)) => do
-    match ← expandCDot? e with
+    match (← expandCDot? e) with
     | some e => `(($e : $type))
     | none   => Macro.throwUnsupported
   | `(($e))         => return (← expandCDot? e).getD e
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 9965bac96a..c7f1e721b9 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -277,7 +277,7 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
       else do
         trace `Elab.command fun _ => stx;
         let s ← get
-        match ← liftMacroM <| expandMacroImpl? s.env stx with
+        match (← liftMacroM <| expandMacroImpl? s.env stx) with
         | some (decl, stxNew) =>
           MonadRef.withElaborator decl do
             withInfoTreeContext (mkInfoTree := mkInfoTree decl stx) do
diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean
index cd0a193f7c..53ff7919be 100644
--- a/src/Lean/Elab/Frontend.lean
+++ b/src/Lean/Elab/Frontend.lean
@@ -27,7 +27,7 @@ def setCommandState (commandState : Command.State) : FrontendM Unit :=
   let ctx ← read
   let s ← get
   let cmdCtx : Command.Context := { cmdPos := s.cmdPos, fileName := ctx.inputCtx.fileName, fileMap := ctx.inputCtx.fileMap }
-  match ← liftM <| EIO.toIO' <| (x cmdCtx).run s.commandState with
+  match (← liftM <| EIO.toIO' <| (x cmdCtx).run s.commandState) with
   | Except.error e      => throw <| IO.Error.userError s!"unexpected internal error: {← e.toMessageData.toString}"
   | Except.ok (a, sNew) => setCommandState sNew; return a
 
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 81394db4c7..3692806d3d 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -741,7 +741,7 @@ private def elabPatterns (patternStxs : Array Syntax) (matchType : Expr) : Excep
             restoreState s
             match (← liftM <| commitIfNoErrors? <| withoutErrToSorry do elabTermAndSynthesize patternStx (← eraseIndices d)) with
             | some pattern =>
-              match ← findDiscrRefinementPath pattern d |>.run with
+              match (← findDiscrRefinementPath pattern d |>.run) with
               | some path =>
                 trace[Meta.debug] "refinement path: {path}"
                 restoreState s
@@ -987,7 +987,7 @@ where
       : TermElabM (Array Expr × Expr × Array (AltLHS × Expr) × Bool) := do
     let s ← saveState
     let (discrs', matchType', altViews', refined) ← generalize discrs matchType altViews generalizing?
-    match ← altViews'.mapM (fun altView => elabMatchAltView altView matchType') |>.run with
+    match (← altViews'.mapM (fun altView => elabMatchAltView altView matchType') |>.run) with
     | Except.ok alts => return (discrs', matchType', alts, first?.isSome || refined)
     | Except.error { patternIdx := patternIdx, pathToIndex := pathToIndex, ex := ex } =>
       trace[Meta.debug] "pathToIndex: {toString pathToIndex}"
@@ -1332,7 +1332,7 @@ builtin_initialize
 @[builtinTermElab «nomatch»] def elabNoMatch : TermElab := fun stx expectedType? => do
   match stx with
   | `(nomatch $discrExpr) =>
-    match ← isLocalIdent? discrExpr with
+    match (← isLocalIdent? discrExpr) with
     | some _ =>
       let expectedType ← waitExpectedType expectedType?
       let discr := Syntax.node ``Lean.Parser.Term.matchDiscr #[mkNullNode, discrExpr]
diff --git a/src/Lean/Elab/PreDefinition/MkInhabitant.lean b/src/Lean/Elab/PreDefinition/MkInhabitant.lean
index ab536ddfbd..42f7e38014 100644
--- a/src/Lean/Elab/PreDefinition/MkInhabitant.lean
+++ b/src/Lean/Elab/PreDefinition/MkInhabitant.lean
@@ -22,7 +22,7 @@ private def mkFnInhabitant? (xs : Array Expr) (type : Expr) : MetaM (Option Expr
     | i+1, type => do
       let x := xs[i]
       let type ← mkForallFVars #[x] type;
-      match ← mkInhabitant? type with
+      match (← mkInhabitant? type) with
       | none     => loop i type
       | some val => pure $ some (← mkLambdaFVars xs[0:i] val)
   loop xs.size type
@@ -30,13 +30,13 @@ private def mkFnInhabitant? (xs : Array Expr) (type : Expr) : MetaM (Option Expr
 /- TODO: add a global IO.Ref to let users customize/extend this procedure -/
 
 def mkInhabitantFor (declName : Name) (xs : Array Expr) (type : Expr) : MetaM Expr := do
-  match ← mkInhabitant? type with
+  match (← mkInhabitant? type) with
   | some val => mkLambdaFVars xs val
   | none     =>
-  match ← findAssumption? xs type with
+  match (← findAssumption? xs type) with
   | some x => mkLambdaFVars xs x
   | none   =>
-  match ← mkFnInhabitant? xs type with
+  match (← mkFnInhabitant? xs type) with
   | some val => pure val
   | none => throwError "failed to compile partial definition '{declName}', failed to show that type is inhabited"
 
diff --git a/src/Lean/Elab/PreDefinition/Structural.lean b/src/Lean/Elab/PreDefinition/Structural.lean
index a27be7d38c..2e8c4420a9 100644
--- a/src/Lean/Elab/PreDefinition/Structural.lean
+++ b/src/Lean/Elab/PreDefinition/Structural.lean
@@ -159,13 +159,13 @@ private partial def findRecArg {α} (numFixed : Nat) (xs : Array Expr) (k : RecA
             let numFixed    := if indexMinPos < numFixed then indexMinPos else numFixed
             let fixedParams := xs.extract 0 numFixed
             let ys          := xs.extract numFixed xs.size
-            match ← hasBadIndexDep? ys indIndices with
+            match (← hasBadIndexDep? ys indIndices) with
             | some (index, y) =>
               orelse'
                 (throwError "argument #{i+1} was not used because its type is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}")
                 (loop (i+1))
             | none =>
-              match ← hasBadParamDep? ys indParams with
+              match (← hasBadParamDep? ys indParams) with
               | some (indParam, y) =>
                 orelse'
                   (throwError "argument #{i+1} was not used because its type is an inductive datatype{indentExpr xType}\nand parameter{indentExpr indParam}\ndepends on{indentExpr y}")
@@ -390,7 +390,7 @@ private partial def replaceIndPredRecApps (recFnName : Name) (recArgInfo : RecAr
               throwError "could not solve using backwards chaining {MessageData.ofGoal main.mvarId!}"
           else
             return mkAppN (← loop f) (← args.mapM loop)
-      match ←matchMatcherApp? e with
+      match (←matchMatcherApp? e) with
       | some matcherApp =>
         if !recArgHasLooseBVarsAt recFnName recArgInfo e then
           processApp e
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 44a7414aba..bd21bab657 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -433,7 +433,7 @@ private def deduplicate (floatedLetDecls : Array Syntax) : Alt → TermElabM (Ar
       -- looks simple enough/created by this function, skip
       return (floatedLetDecls, (pats, rhs))
     withFreshMacroScope do
-      match ← getPatternsVars pats.toArray with
+      match (← getPatternsVars pats.toArray) with
       | #[] =>
         -- no antiquotations => introduce Unit parameter to preserve evaluation order
         let rhs' ← `(rhs Unit.unit)
diff --git a/src/Lean/Elab/Tactic/Injection.lean b/src/Lean/Elab/Tactic/Injection.lean
index 0e79fedcd9..5482282064 100644
--- a/src/Lean/Elab/Tactic/Injection.lean
+++ b/src/Lean/Elab/Tactic/Injection.lean
@@ -23,7 +23,7 @@ private def checkUnusedIds (mvarId : MVarId) (unusedIds : List Name) : MetaM Uni
   let fvarId ← elabAsFVar stx[1]
   let ids := getInjectionNewIds stx[2]
   liftMetaTactic fun mvarId => do
-    match ← Meta.injection mvarId fvarId ids (!ids.isEmpty) with
+    match (← Meta.injection mvarId fvarId ids (!ids.isEmpty)) with
     | Meta.InjectionResult.solved                      => checkUnusedIds mvarId ids; pure []
     | Meta.InjectionResult.subgoal mvarId' _ unusedIds => checkUnusedIds mvarId unusedIds; pure [mvarId']
 
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 33a311f468..e8b4768148 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1135,7 +1135,7 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone :
     checkMaxHeartbeats "elaborator"
     withNestedTraces do
     let env ← getEnv
-    match ← liftMacroM (expandMacroImpl? env stx) with
+    match (← liftMacroM (expandMacroImpl? env stx)) with
     | some (decl, stxNew) =>
       MonadRef.withElaborator decl <|
         withInfoContext' (mkInfo := mkTermInfo (expectedType? := expectedType?) stx) <|
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index 1fc0fca766..f9824d84db 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -139,7 +139,7 @@ def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEn
   let methods := Macro.mkMethods {
     -- TODO: record recursive expansions in info tree?
     expandMacro?     := fun stx => do
-      match ← expandMacroImpl? env stx with
+      match (← expandMacroImpl? env stx) with
       | some (_, stx) => some stx
       | none          => none
     hasDecl          := fun declName => return env.contains declName
diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index 9aa7bd8d92..33774cc6f7 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -16,7 +16,7 @@ def synthesizeArgs (lemmaName : Name) (xs : Array Expr) (bis : Array BinderInfo)
         return false
     else if (← instantiateMVars x).isMVar then
       if (← isProp type) then
-        match ← discharge? type with
+        match (← discharge? type) with
         | some proof =>
           unless (← isDefEq x proof) do
             trace[Meta.Tactic.simp.discharge] "{lemmaName}, failed to assign proof{indentExpr type}"
@@ -30,7 +30,7 @@ def synthesizeArgs (lemmaName : Name) (xs : Array Expr) (bis : Array BinderInfo)
   return true
 where
   synthesizeInstance (x type : Expr) : SimpM Bool := do
-    match ← trySynthInstance type with
+    match (← trySynthInstance type) with
     | LOption.some val =>
       if (← isDefEq x val) then
         return true
diff --git a/src/Lean/ReducibilityAttrs.lean b/src/Lean/ReducibilityAttrs.lean
index 6545f7c83e..84a05d74a9 100644
--- a/src/Lean/ReducibilityAttrs.lean
+++ b/src/Lean/ReducibilityAttrs.lean
@@ -39,7 +39,7 @@ def setReducibleAttribute {m} [Monad m] [MonadEnv m] (declName : Name) : m Unit
   setReducibilityStatus declName ReducibilityStatus.reducible
 
 def isReducible {m} [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
-  match ← getReducibilityStatus declName with
+  match (← getReducibilityStatus declName) with
   | ReducibilityStatus.reducible => true
   | _ => false
 
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index dfbff63e09..d44845d5fa 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -146,7 +146,7 @@ section Initialization
     let opts := {}  -- TODO
     let inputCtx := Parser.mkInputContext m.text.source "<input>"
     let (headerStx, headerParserState, msgLog) ← Parser.parseHeader inputCtx
-    let leanpkgPath ← match ← IO.getEnv "LEAN_SYSROOT" with
+    let leanpkgPath ← match (← IO.getEnv "LEAN_SYSROOT") with
       | some path => pure <| System.FilePath.mk path / "bin" / "leanpkg"
       | _         => pure <| (← appDir) / "leanpkg"
     let leanpkgPath := leanpkgPath.withExtension System.FilePath.exeExtension
diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean
index ceb13dbdbd..daba501099 100644
--- a/src/Lean/Server/Requests.lean
+++ b/src/Lean/Server/Requests.lean
@@ -75,7 +75,7 @@ def mapTask (t : Task α) (f : α → RequestM β) : RequestM (RequestTask β) :
 
 def bindTask (t : Task α) (f : α → RequestM (RequestTask β)) : RequestM (RequestTask β) := fun rc => do
   let t ← IO.bindTask t fun a => do
-    match ← f a rc with
+    match (← f a rc) with
     | Except.error e => return Task.pure <| Except.ok <| Except.error e
     | Except.ok t    => return t.map Except.ok
   return t.map fun
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index e62405c353..0963bb4c44 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -185,7 +185,7 @@ def topDown (stx : Syntax) (firstChoiceOnly := false) : TopDown := ⟨firstChoic
 partial instance : ForIn m TopDown Syntax where
   forIn := fun ⟨firstChoiceOnly, stx⟩ init f => do
     let rec @[specialize] loop stx b [Inhabited (typeOf% b)] := do
-      match ← f stx b with
+      match (← f stx b) with
       | ForInStep.yield b' =>
         let mut b := b'
         if let Syntax.node k args := stx then
@@ -193,12 +193,12 @@ partial instance : ForIn m TopDown Syntax where
             return ← loop args[0] b
           else
             for arg in args do
-              match ← loop arg b with
+              match (← loop arg b) with
               | ForInStep.yield b' => b := b'
               | ForInStep.done b'  => return ForInStep.done b'
         return ForInStep.yield b
       | ForInStep.done b => return ForInStep.done b
-    match ← @loop stx init ⟨init⟩ with
+    match (← @loop stx init ⟨init⟩) with
     | ForInStep.yield b => return b
     | ForInStep.done b  => return b
 
diff --git a/src/Std/Data/RBMap.lean b/src/Std/Data/RBMap.lean
index ebeeca1c4c..d6b854d88b 100644
--- a/src/Std/Data/RBMap.lean
+++ b/src/Std/Data/RBMap.lean
@@ -53,7 +53,7 @@ protected def max : RBNode α β → Option (Sigma (fun k => β k))
         match (← f k v b) with
         | r@(ForInStep.done _) => return r
         | ForInStep.yield b    => visit r b
-  match ← visit as init with
+  match (← visit as init) with
   | ForInStep.done b  => pure b
   | ForInStep.yield b => pure b