diff --git a/library/Init/Data/PersistentArray/Basic.lean b/library/Init/Data/PersistentArray/Basic.lean
index 1363ab00c5..dacc0ee2af 100644
--- a/library/Init/Data/PersistentArray/Basic.lean
+++ b/library/Init/Data/PersistentArray/Basic.lean
@@ -260,10 +260,9 @@ variable {β : Type u}
 | leaf vs => leaf <$> vs.mmap f
 
 @[specialize] def mmap (f : α → m β) (t : PersistentArray α) : m (PersistentArray β) :=
-do
-  root ← mmapAux f t.root;
-  tail ← t.tail.mmap f;
-  pure { tail := tail, root := root, .. t }
+do root ← mmapAux f t.root;
+   tail ← t.tail.mmap f;
+   pure { tail := tail, root := root, .. t }
 
 end
 
diff --git a/library/Init/Lean/Compiler/IR/Borrow.lean b/library/Init/Lean/Compiler/IR/Borrow.lean
index 6f537da9f6..6e2dc1e2e3 100644
--- a/library/Init/Lean/Compiler/IR/Borrow.lean
+++ b/library/Init/Lean/Compiler/IR/Borrow.lean
@@ -161,31 +161,29 @@ do s ← get;
 
 /- Updates `map[k]` using the current set of `owned` variables. -/
 def updateParamMap (k : Key) : M Unit :=
-do
-s ← get;
-match s.map.find k with
-| some ps => do
-  ps ← ps.mmap $ fun (p : Param) =>
-   if p.borrow && s.owned.contains p.x.idx then do
-     markModifiedParamMap; pure { borrow := false, .. p }
-   else
-     pure p;
-  modify $ fun s => { map := s.map.insert k ps, .. s }
-| none    => pure ()
+do s ← get;
+   match s.map.find k with
+   | some ps => do
+     ps ← ps.mmap $ fun (p : Param) =>
+      if p.borrow && s.owned.contains p.x.idx then do
+        markModifiedParamMap; pure { borrow := false, .. p }
+      else
+        pure p;
+     modify $ fun s => { map := s.map.insert k ps, .. s }
+   | none    => pure ()
 
 def getParamInfo (k : Key) : M (Array Param) :=
-do
-s ← get;
-match s.map.find k with
-| some ps => pure ps
-| none    =>
-  match k with
-  | (Key.decl fn) => do
-    ctx ← read;
-    match findEnvDecl ctx.env fn with
-    | some decl => pure decl.params
-    | none      => pure Array.empty   -- unreachable if well-formed input
-  | _ => pure Array.empty -- unreachable if well-formed input
+do s ← get;
+   match s.map.find k with
+   | some ps => pure ps
+   | none    =>
+     match k with
+     | (Key.decl fn) => do
+       ctx ← read;
+       match findEnvDecl ctx.env fn with
+       | some decl => pure decl.params
+       | none      => pure Array.empty   -- unreachable if well-formed input
+     | _ => pure Array.empty -- unreachable if well-formed input
 
 /- For each ps[i], if ps[i] is owned, then mark xs[i] as owned. -/
 def ownArgsUsingParams (xs : Array Arg) (ps : Array Param) : M Unit :=
@@ -218,12 +216,11 @@ xs.size.mfor $ fun i => do
    ```
 -/
 def ownArgsIfParam (xs : Array Arg) : M Unit :=
-do
-ctx ← read;
-xs.mfor $ fun x =>
-  match x with
-  | Arg.var x => when (ctx.paramSet.contains x.idx) $ ownVar x
-  | _ => pure ()
+do ctx ← read;
+   xs.mfor $ fun x =>
+     match x with
+     | Arg.var x => when (ctx.paramSet.contains x.idx) $ ownVar x
+     | _ => pure ()
 
 def collectExpr (z : VarId) : Expr → M Unit
 | Expr.reset _ x      => ownVar z *> ownVar x
@@ -300,10 +297,9 @@ partial def collectDecl : Decl → M Unit
 whileModifingParamMapAux x ()
 
 def collectDecls (decls : Array Decl) : M ParamMap :=
-do
-whileModifingParamMap (decls.mfor collectDecl);
-s ← get;
-pure s.map
+do whileModifingParamMap (decls.mfor collectDecl);
+   s ← get;
+   pure s.map
 
 def infer (env : Environment) (decls : Array Decl) : ParamMap :=
 (collectDecls decls { env := env }).run' { map := mkInitParamMap env decls }
@@ -311,11 +307,10 @@ def infer (env : Environment) (decls : Array Decl) : ParamMap :=
 end Borrow
 
 def inferBorrow (decls : Array Decl) : CompilerM (Array Decl) :=
-do
-env ← getEnv;
-let decls    := decls.map Decl.normalizeIds;
-let paramMap := Borrow.infer env decls;
-pure (Borrow.applyParamMap decls paramMap)
+do env ← getEnv;
+   let decls    := decls.map Decl.normalizeIds;
+   let paramMap := Borrow.infer env decls;
+   pure (Borrow.applyParamMap decls paramMap)
 
 end IR
 end Lean
diff --git a/library/Init/Lean/Compiler/IR/Boxing.lean b/library/Init/Lean/Compiler/IR/Boxing.lean
index f6b3399a8a..9ceaf91be2 100644
--- a/library/Init/Lean/Compiler/IR/Boxing.lean
+++ b/library/Init/Lean/Compiler/IR/Boxing.lean
@@ -51,30 +51,29 @@ let ps := decl.params;
 || ps.size > closureMaxArgs
 
 def mkBoxedVersionAux (decl : Decl) : N Decl :=
-do
-let ps := decl.params;
-qs ← ps.mmap (fun _ => do x ← mkFresh; pure { Param . x := x, ty := IRType.object, borrow := false });
-(newVDecls, xs) ← qs.size.mfold
-  (fun i (r : Array FnBody × Array Arg) =>
-     let (newVDecls, xs) := r;
-     let p := ps.get! i;
-     let q := qs.get! i;
-     if !p.ty.isScalar then pure (newVDecls, xs.push (Arg.var q.x))
-     else do
-       x ← mkFresh;
-       pure (newVDecls.push (FnBody.vdecl x p.ty (Expr.unbox q.x) (default _)), xs.push (Arg.var x)))
-  (Array.empty, Array.empty);
-r ← mkFresh;
-let newVDecls := newVDecls.push (FnBody.vdecl r decl.resultType (Expr.fap decl.name xs) (default _));
-body ←
- if !decl.resultType.isScalar then do {
-   pure $ reshape newVDecls (FnBody.ret (Arg.var r))
- } else do {
-   newR ← mkFresh;
-   let newVDecls := newVDecls.push (FnBody.vdecl newR IRType.object (Expr.box decl.resultType r) (default _));
-   pure $ reshape newVDecls (FnBody.ret (Arg.var newR))
- };
-pure $ Decl.fdecl (mkBoxedName decl.name) qs IRType.object body
+do let ps := decl.params;
+   qs ← ps.mmap (fun _ => do x ← mkFresh; pure { Param . x := x, ty := IRType.object, borrow := false });
+   (newVDecls, xs) ← qs.size.mfold
+     (fun i (r : Array FnBody × Array Arg) =>
+        let (newVDecls, xs) := r;
+        let p := ps.get! i;
+        let q := qs.get! i;
+        if !p.ty.isScalar then pure (newVDecls, xs.push (Arg.var q.x))
+        else do
+          x ← mkFresh;
+          pure (newVDecls.push (FnBody.vdecl x p.ty (Expr.unbox q.x) (default _)), xs.push (Arg.var x)))
+     (Array.empty, Array.empty);
+   r ← mkFresh;
+   let newVDecls := newVDecls.push (FnBody.vdecl r decl.resultType (Expr.fap decl.name xs) (default _));
+   body ←
+     if !decl.resultType.isScalar then do {
+       pure $ reshape newVDecls (FnBody.ret (Arg.var r))
+     } else do {
+       newR ← mkFresh;
+       let newVDecls := newVDecls.push (FnBody.vdecl newR IRType.object (Expr.box decl.resultType r) (default _));
+       pure $ reshape newVDecls (FnBody.ret (Arg.var newR))
+     };
+   pure $ Decl.fdecl (mkBoxedName decl.name) qs IRType.object body
 
 def mkBoxedVersion (decl : Decl) : Decl :=
 (mkBoxedVersionAux decl).run' 1
@@ -181,37 +180,36 @@ else match xType with
    It is used when the expected type does not match `xType`.
    If `xType` is scalar, then we need to "box" it. Otherwise, we need to "unbox" it. -/
 def mkCast (x : VarId) (xType : IRType) (expectedType : IRType) : M Expr :=
-do
-optVal ← isExpensiveConstantValueBoxing x xType;
-match optVal with
-| some v => do
-  ctx ← read;
-  s ← get;
-  /- Create auxiliary FnBody
+do optVal ← isExpensiveConstantValueBoxing x xType;
+   match optVal with
+   | some v => do
+     ctx ← read;
+     s ← get;
+     /- Create auxiliary FnBody
      ```
      let x_1 : xType := v;
      let x_2 : expectedType := Expr.box xType x_1;
      ret x_2
      ```
-   -/
-  let body : FnBody :=
-    FnBody.vdecl { idx := 1 } xType v $
-    FnBody.vdecl { idx := 2 } expectedType (Expr.box xType { idx := 1 }) $
-    FnBody.ret (mkVarArg { idx := 2 });
-  match s.auxDeclCache.find body with
-  | some v => pure v
-  | none   => do
-    let auxName  := ctx.f ++ ((`_boxed_const).appendIndexAfter s.nextAuxId);
-    let auxConst := Expr.fap auxName Array.empty;
-    let auxDecl  := Decl.fdecl auxName Array.empty expectedType body;
-    modify $ fun s => {
-     auxDecls     := s.auxDecls.push auxDecl,
-     auxDeclCache := s.auxDeclCache.cons body auxConst,
-     nextAuxId    := s.nextAuxId + 1,
-     .. s
-    };
-    pure auxConst
-| none => pure $ if xType.isScalar then Expr.box xType x else Expr.unbox x
+     -/
+     let body : FnBody :=
+       FnBody.vdecl { idx := 1 } xType v $
+       FnBody.vdecl { idx := 2 } expectedType (Expr.box xType { idx := 1 }) $
+       FnBody.ret (mkVarArg { idx := 2 });
+     match s.auxDeclCache.find body with
+     | some v => pure v
+     | none   => do
+       let auxName  := ctx.f ++ ((`_boxed_const).appendIndexAfter s.nextAuxId);
+       let auxConst := Expr.fap auxName Array.empty;
+       let auxDecl  := Decl.fdecl auxName Array.empty expectedType body;
+       modify $ fun s => {
+        auxDecls     := s.auxDecls.push auxDecl,
+        auxDeclCache := s.auxDeclCache.cons body auxConst,
+        nextAuxId    := s.nextAuxId + 1,
+        .. s
+       };
+       pure auxConst
+   | none => pure $ if xType.isScalar then Expr.box xType x else Expr.unbox x
 
 @[inline] def castVarIfNeeded (x : VarId) (expected : IRType) (k : VarId → M FnBody) : M FnBody :=
 do xType ← getVarType x;
diff --git a/library/Init/Lean/Compiler/IR/Checker.lean b/library/Init/Lean/Compiler/IR/Checker.lean
index 31af550acf..0c9827cb2a 100644
--- a/library/Init/Lean/Compiler/IR/Checker.lean
+++ b/library/Init/Lean/Compiler/IR/Checker.lean
@@ -58,16 +58,14 @@ def checkScalarVar (x : VarId) : M Unit :=
 checkVarType x IRType.isScalar
 
 def checkFullApp (c : FunId) (ys : Array Arg) : M Unit :=
-do
-decl ← getDecl c;
-unless (ys.size == decl.params.size) (throw ("incorrect number of arguments to '" ++ toString c ++ "', " ++ toString ys.size ++ " provided, " ++ toString decl.params.size ++ " expected"));
-checkArgs ys
+do decl ← getDecl c;
+   unless (ys.size == decl.params.size) (throw ("incorrect number of arguments to '" ++ toString c ++ "', " ++ toString ys.size ++ " provided, " ++ toString decl.params.size ++ " expected"));
+   checkArgs ys
 
 def checkPartialApp (c : FunId) (ys : Array Arg) : M Unit :=
-do
-decl ← getDecl c;
-unless (ys.size < decl.params.size) (throw ("too many arguments too partial application '" ++ toString c ++ "', num. args: " ++ toString ys.size ++ ", arity: " ++ toString decl.params.size));
-checkArgs ys
+do decl ← getDecl c;
+   unless (ys.size < decl.params.size) (throw ("too many arguments too partial application '" ++ toString c ++ "', num. args: " ++ toString ys.size ++ ", arity: " ++ toString decl.params.size));
+   checkArgs ys
 
 def checkExpr (ty : IRType) : Expr → M Unit
 | Expr.pap f ys           => checkPartialApp f ys *> checkObjType ty -- partial applications should always produce a closure object
@@ -124,11 +122,10 @@ def checkDecl : Decl → M Unit
 end Checker
 
 def checkDecl (decls : Array Decl) (decl : Decl) : CompilerM Unit :=
-do
-env ← getEnv;
-match Checker.checkDecl decl { env := env, decls := decls } with
-| Except.error msg => throw ("IR check failed at '" ++ toString decl.name ++ "', error: " ++ msg)
-| other            => pure ()
+do env ← getEnv;
+   match Checker.checkDecl decl { env := env, decls := decls } with
+   | Except.error msg => throw ("IR check failed at '" ++ toString decl.name ++ "', error: " ++ msg)
+   | other            => pure ()
 
 def checkDecls (decls : Array Decl) : CompilerM Unit :=
 decls.mfor (checkDecl decls)
diff --git a/library/Init/Lean/Compiler/IR/Default.lean b/library/Init/Lean/Compiler/IR/Default.lean
index 35b1254e9b..2af52a612a 100644
--- a/library/Init/Lean/Compiler/IR/Default.lean
+++ b/library/Init/Lean/Compiler/IR/Default.lean
@@ -25,34 +25,33 @@ namespace Lean
 namespace IR
 
 private def compileAux (decls : Array Decl) : CompilerM Unit :=
-do
-logDecls `init decls;
-checkDecls decls;
-decls ← elimDeadBranches decls;
-logDecls `elim_dead_branches decls;
-let decls := decls.map Decl.pushProj;
-logDecls `push_proj decls;
-let decls := decls.map Decl.insertResetReuse;
-logDecls `reset_reuse decls;
-let decls := decls.map Decl.elimDead;
-logDecls `elim_dead decls;
-let decls := decls.map Decl.simpCase;
-logDecls `simp_case decls;
-let decls := decls.map Decl.normalizeIds;
-decls ← inferBorrow decls;
-logDecls `borrow decls;
-decls ← explicitBoxing decls;
-logDecls `boxing decls;
-decls ← explicitRC decls;
-logDecls `rc decls;
-let decls := decls.map Decl.expandResetReuse;
-logDecls `expand_reset_reuse decls;
-let decls := decls.map Decl.pushProj;
-logDecls `push_proj decls;
-logDecls `result decls;
-checkDecls decls;
-addDecls decls;
-pure ()
+do logDecls `init decls;
+   checkDecls decls;
+   decls ← elimDeadBranches decls;
+   logDecls `elim_dead_branches decls;
+   let decls := decls.map Decl.pushProj;
+   logDecls `push_proj decls;
+   let decls := decls.map Decl.insertResetReuse;
+   logDecls `reset_reuse decls;
+   let decls := decls.map Decl.elimDead;
+   logDecls `elim_dead decls;
+   let decls := decls.map Decl.simpCase;
+   logDecls `simp_case decls;
+   let decls := decls.map Decl.normalizeIds;
+   decls ← inferBorrow decls;
+   logDecls `borrow decls;
+   decls ← explicitBoxing decls;
+   logDecls `boxing decls;
+   decls ← explicitRC decls;
+   logDecls `rc decls;
+   let decls := decls.map Decl.expandResetReuse;
+   logDecls `expand_reset_reuse decls;
+   let decls := decls.map Decl.pushProj;
+   logDecls `push_proj decls;
+   logDecls `result decls;
+   checkDecls decls;
+   addDecls decls;
+   pure ()
 
 @[export lean_ir_compile]
 def compile (env : Environment) (opts : Options) (decls : Array Decl) : Log × (Except String Environment) :=
@@ -61,15 +60,14 @@ match (compileAux decls opts).run { env := env } with
 | EState.Result.error msg s => (s.log, Except.error msg)
 
 def addBoxedVersionAux (decl : Decl) : CompilerM Unit :=
-do
-env ← getEnv;
-if !ExplicitBoxing.requiresBoxedVersion env decl then pure ()
-else do
-  let decl := ExplicitBoxing.mkBoxedVersion decl;
-  let decls : Array Decl := #[decl];
-  decls ← explicitRC decls;
-  decls.mfor $ fun decl => modifyEnv $ fun env => addDeclAux env decl;
-  pure ()
+do env ← getEnv;
+   if !ExplicitBoxing.requiresBoxedVersion env decl then pure ()
+   else do
+     let decl := ExplicitBoxing.mkBoxedVersion decl;
+     let decls : Array Decl := #[decl];
+     decls ← explicitRC decls;
+     decls.mfor $ fun decl => modifyEnv $ fun env => addDeclAux env decl;
+     pure ()
 
 -- Remark: we are ignoring the `Log` here. This should be fine.
 @[export lean_ir_add_boxed_version]
diff --git a/library/Init/Lean/Compiler/IR/EmitC.lean b/library/Init/Lean/Compiler/IR/EmitC.lean
index e6c6f640c4..caa8e7d8c3 100644
--- a/library/Init/Lean/Compiler/IR/EmitC.lean
+++ b/library/Init/Lean/Compiler/IR/EmitC.lean
@@ -93,96 +93,91 @@ def emitCInitName (n : Name) : M Unit :=
 toCInitName n >>= emit
 
 def emitFnDeclAux (decl : Decl) (cppBaseName : String) (addExternForConsts : Bool) : M Unit :=
-do
-let ps := decl.params;
-when (ps.isEmpty && addExternForConsts) (emit "extern ");
-emit (toCType decl.resultType ++ " " ++ cppBaseName);
-unless (ps.isEmpty) $ do {
-  emit "(";
-  if ps.size > closureMaxArgs && isBoxedName decl.name then
-    emit "lean_object**"
-  else
-    ps.size.mfor $ fun i => do {
-      when (i > 0) (emit ", ");
-      emit (toCType (ps.get! i).ty)
-    };
-  emit ")"
-};
-emitLn ";"
+do let ps := decl.params;
+   when (ps.isEmpty && addExternForConsts) (emit "extern ");
+   emit (toCType decl.resultType ++ " " ++ cppBaseName);
+   unless (ps.isEmpty) $ do {
+     emit "(";
+     if ps.size > closureMaxArgs && isBoxedName decl.name then
+       emit "lean_object**"
+     else
+       ps.size.mfor $ fun i => do {
+         when (i > 0) (emit ", ");
+         emit (toCType (ps.get! i).ty)
+       };
+     emit ")"
+   };
+   emitLn ";"
 
 def emitFnDecl (decl : Decl) (addExternForConsts : Bool) : M Unit :=
-do
-cppBaseName ← toCName decl.name;
-emitFnDeclAux decl cppBaseName addExternForConsts
+do cppBaseName ← toCName decl.name;
+   emitFnDeclAux decl cppBaseName addExternForConsts
 
 def emitExternDeclAux (decl : Decl) (cNameStr : String) : M Unit :=
-do
-let cName := mkSimpleName cNameStr;
-env ← getEnv;
-let extC := isExternC env decl.name;
-emitFnDeclAux decl cNameStr (!extC)
+do let cName := mkSimpleName cNameStr;
+   env ← getEnv;
+   let extC := isExternC env decl.name;
+   emitFnDeclAux decl cNameStr (!extC)
 
 def emitFnDecls : M Unit :=
-do
-env ← getEnv;
-let decls := getDecls env;
-let modDecls  : NameSet := decls.foldl (fun s d => s.insert d.name) {};
-let usedDecls : NameSet := decls.foldl (fun s d => collectUsedDecls env d (s.insert d.name)) {};
-let usedDecls := usedDecls.toList;
-usedDecls.mfor $ fun n => do
-  decl ← getDecl n;
-  match getExternNameFor env `c decl.name with
-  | some cName => emitExternDeclAux decl cName
-  | none       => emitFnDecl decl (!modDecls.contains n)
+do env ← getEnv;
+   let decls := getDecls env;
+   let modDecls  : NameSet := decls.foldl (fun s d => s.insert d.name) {};
+   let usedDecls : NameSet := decls.foldl (fun s d => collectUsedDecls env d (s.insert d.name)) {};
+   let usedDecls := usedDecls.toList;
+   usedDecls.mfor $ fun n => do
+     decl ← getDecl n;
+     match getExternNameFor env `c decl.name with
+     | some cName => emitExternDeclAux decl cName
+     | none       => emitFnDecl decl (!modDecls.contains n)
 
 def emitMainFn : M Unit :=
-do
-d ← getDecl `main;
-match d with
-| Decl.fdecl f xs t b => do
-  unless (xs.size == 2 || xs.size == 1) (throw "invalid main function, incorrect arity when generating code");
-  env ← getEnv;
-  let usesLeanAPI := usesLeanNamespace env d;
-  if usesLeanAPI then
-    emitLn "void lean_initialize();"
-  else
-    emitLn "void lean_initialize_runtime_module();";
-  emitLn "int main(int argc, char ** argv) {\nlean_object* w; lean_object* in;";
-  if usesLeanAPI then
-    emitLn "lean_initialize();"
-  else
-    emitLn "lean_initialize_runtime_module();";
-  emitLn "w = lean_io_mk_world();";
-  modName ← getModName;
-  emitLn ("w = initialize_" ++ (modName.mangle "") ++ "(w);");
-  emitLns ["lean_io_mark_end_initialization();",
-           "if (lean_io_result_is_ok(w)) {",
-           "lean_init_task_manager();"];
-  if xs.size == 2 then do {
-    emitLns ["in = lean_box(0);",
-             "int i = argc;",
-             "while (i > 1) {",
-             " lean_object* n;",
-             " i--;",
-             " n = lean_alloc_ctor(1,2,0); lean_ctor_set(n, 0, lean_mk_string(argv[i])); lean_ctor_set(n, 1, in);",
-             " in = n;",
-             "}"];
-    emitLn ("w = " ++ leanMainFn ++ "(in, w);")
-  } else do {
-    emitLn ("w = " ++ leanMainFn ++ "(w);")
-  };
-  emitLn "}";
-  emitLns ["if (lean_io_result_is_ok(w)) {",
-           "  int ret = lean_unbox(lean_io_result_get_value(w));",
-           "  lean_dec_ref(w);",
-           "  return ret;",
-           "} else {",
-           "  lean_io_result_show_error(w);",
-           "  lean_dec_ref(w);",
-           "  return 1;",
-           "}"];
-  emitLn "}"
-| other => throw "function declaration expected"
+do d ← getDecl `main;
+   match d with
+   | Decl.fdecl f xs t b => do
+     unless (xs.size == 2 || xs.size == 1) (throw "invalid main function, incorrect arity when generating code");
+     env ← getEnv;
+     let usesLeanAPI := usesLeanNamespace env d;
+     if usesLeanAPI then
+       emitLn "void lean_initialize();"
+     else
+       emitLn "void lean_initialize_runtime_module();";
+     emitLn "int main(int argc, char ** argv) {\nlean_object* w; lean_object* in;";
+     if usesLeanAPI then
+       emitLn "lean_initialize();"
+     else
+       emitLn "lean_initialize_runtime_module();";
+     emitLn "w = lean_io_mk_world();";
+     modName ← getModName;
+     emitLn ("w = initialize_" ++ (modName.mangle "") ++ "(w);");
+     emitLns ["lean_io_mark_end_initialization();",
+              "if (lean_io_result_is_ok(w)) {",
+              "lean_init_task_manager();"];
+     if xs.size == 2 then do {
+       emitLns ["in = lean_box(0);",
+                "int i = argc;",
+                "while (i > 1) {",
+                " lean_object* n;",
+                " i--;",
+                " n = lean_alloc_ctor(1,2,0); lean_ctor_set(n, 0, lean_mk_string(argv[i])); lean_ctor_set(n, 1, in);",
+                " in = n;",
+               "}"];
+       emitLn ("w = " ++ leanMainFn ++ "(in, w);")
+     } else do {
+       emitLn ("w = " ++ leanMainFn ++ "(w);")
+     };
+     emitLn "}";
+     emitLns ["if (lean_io_result_is_ok(w)) {",
+              "  int ret = lean_unbox(lean_io_result_get_value(w));",
+              "  lean_dec_ref(w);",
+              "  return ret;",
+              "} else {",
+              "  lean_io_result_show_error(w);",
+              "  lean_dec_ref(w);",
+              "  return 1;",
+              "}"];
+     emitLn "}"
+   | other => throw "function declaration expected"
 
 def hasMainFn : M Bool :=
 do env ← getEnv;
@@ -193,28 +188,27 @@ def emitMainFnIfNeeded : M Unit :=
 mwhen hasMainFn emitMainFn
 
 def emitFileHeader : M Unit :=
-do
-env ← getEnv;
-modName ← getModName;
-emitLn "// Lean compiler output";
-emitLn ("// Module: " ++ toString modName);
-emit "// Imports:";
-env.imports.mfor $ fun m => emit (" " ++ toString m);
-emitLn "";
-emitLn "#include \"runtime/lean.h\"";
-emitLns [
- "#if defined(__clang__)",
- "#pragma clang diagnostic ignored \"-Wunused-parameter\"",
- "#pragma clang diagnostic ignored \"-Wunused-label\"",
- "#elif defined(__GNUC__) && !defined(__CLANG__)",
- "#pragma GCC diagnostic ignored \"-Wunused-parameter\"",
- "#pragma GCC diagnostic ignored \"-Wunused-label\"",
- "#pragma GCC diagnostic ignored \"-Wunused-but-set-variable\"",
- "#endif",
- "#ifdef __cplusplus",
- "extern \"C\" {",
- "#endif"
-]
+do env ← getEnv;
+   modName ← getModName;
+   emitLn "// Lean compiler output";
+   emitLn ("// Module: " ++ toString modName);
+   emit "// Imports:";
+   env.imports.mfor $ fun m => emit (" " ++ toString m);
+   emitLn "";
+   emitLn "#include \"runtime/lean.h\"";
+   emitLns [
+    "#if defined(__clang__)",
+    "#pragma clang diagnostic ignored \"-Wunused-parameter\"",
+    "#pragma clang diagnostic ignored \"-Wunused-label\"",
+    "#elif defined(__GNUC__) && !defined(__CLANG__)",
+    "#pragma GCC diagnostic ignored \"-Wunused-parameter\"",
+    "#pragma GCC diagnostic ignored \"-Wunused-label\"",
+    "#pragma GCC diagnostic ignored \"-Wunused-but-set-variable\"",
+    "#endif",
+    "#ifdef __cplusplus",
+    "extern \"C\" {",
+    "#endif"
+  ]
 
 def emitFileFooter : M Unit :=
 emitLns [
@@ -249,11 +243,10 @@ partial def declareVars : FnBody → Bool → M Bool
 | e,                        d => if e.isTerminal then pure d else declareVars e.body d
 
 def emitTag (x : VarId) (xType : IRType) : M Unit :=
-do
-if xType.isObj then do
-  emit "lean_obj_tag("; emit x; emit ")"
-else
-  emit x
+do if xType.isObj then do
+     emit "lean_obj_tag("; emit x; emit ")"
+   else
+     emit x
 
 def isIf (alts : Array Alt) : Option (Nat × FnBody × FnBody) :=
 if alts.size != 2 then none
@@ -262,11 +255,10 @@ else match alts.get! 0 with
   | _            => none
 
 def emitIf (emitBody : FnBody → M Unit) (x : VarId) (xType : IRType) (tag : Nat) (t : FnBody) (e : FnBody) : M Unit :=
-do
-emit "if ("; emitTag x xType; emit " == "; emit tag; emitLn ")";
-emitBody t;
-emitLn "else";
-emitBody e
+do emit "if ("; emitTag x xType; emit " == "; emit tag; emitLn ")";
+   emitBody t;
+   emitLn "else";
+   emitBody e
 
 def emitCase (emitBody : FnBody → M Unit) (x : VarId) (xType : IRType) (alts : Array Alt) : M Unit :=
 match isIf alts with
@@ -280,20 +272,18 @@ match isIf alts with
   emitLn "}"
 
 def emitInc (x : VarId) (n : Nat) (checkRef : Bool) : M Unit :=
-do
-emit $
-  if checkRef then (if n == 1 then "lean_inc" else "lean_inc_n")
-  else (if n == 1 then "lean_inc_ref" else "lean_inc_ref_n");
-emit "(" *> emit x;
-when (n != 1) (emit ", " *> emit n);
-emitLn ");"
+do emit $
+     if checkRef then (if n == 1 then "lean_inc" else "lean_inc_n")
+     else (if n == 1 then "lean_inc_ref" else "lean_inc_ref_n");
+   emit "(" *> emit x;
+   when (n != 1) (emit ", " *> emit n);
+   emitLn ");"
 
 def emitDec (x : VarId) (n : Nat) (checkRef : Bool) : M Unit :=
-do
-emit (if checkRef then "lean_dec" else "lean_dec_ref");
-emit "("; emit x;
-when (n != 1) (do emit ", "; emit n);
-emitLn ");"
+do emit (if checkRef then "lean_dec" else "lean_dec_ref");
+   emit "("; emit x;
+   when (n != 1) (do emit ", "; emit n);
+   emitLn ");"
 
 def emitDel (x : VarId) : M Unit :=
 do emit "lean_free_object("; emit x; emitLn ");"
@@ -315,26 +305,24 @@ def emitUSet (x : VarId) (n : Nat) (y : VarId) : M Unit :=
 do emit "lean_ctor_set_usize("; emit x; emit ", "; emit n; emit ", "; emit y; emitLn ");"
 
 def emitSSet (x : VarId) (n : Nat) (offset : Nat) (y : VarId) (t : IRType) : M Unit :=
-do
-match t with
-| IRType.float  => throw "floats are not supported yet"
-| IRType.uint8  => emit "lean_ctor_set_uint8"
-| IRType.uint16 => emit "lean_ctor_set_uint16"
-| IRType.uint32 => emit "lean_ctor_set_uint32"
-| IRType.uint64 => emit "lean_ctor_set_uint64"
-| _             => throw "invalid instruction";
-emit "("; emit x; emit ", "; emitOffset n offset; emit ", "; emit y; emitLn ");"
+do match t with
+   | IRType.float  => throw "floats are not supported yet"
+   | IRType.uint8  => emit "lean_ctor_set_uint8"
+   | IRType.uint16 => emit "lean_ctor_set_uint16"
+   | IRType.uint32 => emit "lean_ctor_set_uint32"
+   | IRType.uint64 => emit "lean_ctor_set_uint64"
+   | _             => throw "invalid instruction";
+   emit "("; emit x; emit ", "; emitOffset n offset; emit ", "; emit y; emitLn ");"
 
 def emitJmp (j : JoinPointId) (xs : Array Arg) : M Unit :=
-do
-  ps ← getJPParams j;
-  unless (xs.size == ps.size) (throw "invalid goto");
-  xs.size.mfor $ fun i => do {
-    let p := ps.get! i;
-    let x := xs.get! i;
-    emit p.x; emit " = "; emitArg x; emitLn ";"
-  };
-  emit "goto "; emit j; emitLn ";"
+do ps ← getJPParams j;
+   unless (xs.size == ps.size) (throw "invalid goto");
+    xs.size.mfor $ fun i => do {
+      let p := ps.get! i;
+      let x := xs.get! i;
+      emit p.x; emit " = "; emitArg x; emitLn ";"
+    };
+    emit "goto "; emit j; emitLn ";"
 
 def emitLhs (z : VarId) : M Unit :=
 do emit z; emit " = "
@@ -350,43 +338,39 @@ else if ssize == 0 then emit "sizeof(size_t)*" *> emit usize
 else emit "sizeof(size_t)*" *> emit usize *> emit " + " *> emit ssize
 
 def emitAllocCtor (c : CtorInfo) : M Unit :=
-do
-emit "lean_alloc_ctor("; emit c.cidx; emit ", "; emit c.size; emit ", ";
-emitCtorScalarSize c.usize c.ssize; emitLn ");"
+do emit "lean_alloc_ctor("; emit c.cidx; emit ", "; emit c.size; emit ", ";
+   emitCtorScalarSize c.usize c.ssize; emitLn ");"
 
 def emitCtorSetArgs (z : VarId) (ys : Array Arg) : M Unit :=
 ys.size.mfor $ fun i => do
   emit "lean_ctor_set("; emit z; emit ", "; emit i; emit ", "; emitArg (ys.get! i); emitLn ");"
 
 def emitCtor (z : VarId) (c : CtorInfo) (ys : Array Arg) : M Unit :=
-do
-emitLhs z;
-if c.size == 0 && c.usize == 0 && c.ssize == 0 then do
-  emit "lean_box("; emit c.cidx; emitLn ");"
-else do
-  emitAllocCtor c; emitCtorSetArgs z ys
+do emitLhs z;
+   if c.size == 0 && c.usize == 0 && c.ssize == 0 then do
+     emit "lean_box("; emit c.cidx; emitLn ");"
+   else do
+     emitAllocCtor c; emitCtorSetArgs z ys
 
 def emitReset (z : VarId) (n : Nat) (x : VarId) : M Unit :=
-do
-emit "if (lean_is_exclusive("; emit x; emitLn ")) {";
-n.mfor $ fun i => do {
-  emit " lean_ctor_release("; emit x; emit ", "; emit i; emitLn ");"
-};
-emit " "; emitLhs z; emit x; emitLn ";";
-emitLn "} else {";
-emit " lean_dec_ref("; emit x; emitLn ");";
-emit " "; emitLhs z; emitLn "lean_box(0);";
-emitLn "}"
+do emit "if (lean_is_exclusive("; emit x; emitLn ")) {";
+   n.mfor $ fun i => do {
+     emit " lean_ctor_release("; emit x; emit ", "; emit i; emitLn ");"
+   };
+   emit " "; emitLhs z; emit x; emitLn ";";
+   emitLn "} else {";
+   emit " lean_dec_ref("; emit x; emitLn ");";
+   emit " "; emitLhs z; emitLn "lean_box(0);";
+   emitLn "}"
 
 def emitReuse (z : VarId) (x : VarId) (c : CtorInfo) (updtHeader : Bool) (ys : Array Arg) : M Unit :=
-do
-emit "if (lean_is_scalar("; emit x; emitLn ")) {";
-emit " "; emitLhs z; emitAllocCtor c;
-emitLn "} else {";
-emit " "; emitLhs z; emit x; emitLn ";";
-when updtHeader (do emit " lean_ctor_set_tag("; emit z; emit ", "; emit c.cidx; emitLn ");");
-emitLn "}";
-emitCtorSetArgs z ys
+do emit "if (lean_is_scalar("; emit x; emitLn ")) {";
+   emit " "; emitLhs z; emitAllocCtor c;
+   emitLn "} else {";
+   emit " "; emitLhs z; emit x; emitLn ";";
+   when updtHeader (do emit " lean_ctor_set_tag("; emit z; emit ", "; emit c.cidx; emitLn ");");
+   emitLn "}";
+   emitCtorSetArgs z ys
 
 def emitProj (z : VarId) (i : Nat) (x : VarId) : M Unit :=
 do emitLhs z; emit "lean_ctor_get("; emit x; emit ", "; emit i; emitLn ");"
@@ -395,40 +379,37 @@ def emitUProj (z : VarId) (i : Nat) (x : VarId) : M Unit :=
 do emitLhs z; emit "lean_ctor_get_usize("; emit x; emit ", "; emit i; emitLn ");"
 
 def emitSProj (z : VarId) (t : IRType) (n offset : Nat) (x : VarId) : M Unit :=
-do
-emitLhs z;
-match t with
-| IRType.float  => throw "floats are not supported yet"
-| IRType.uint8  => emit "lean_ctor_get_uint8"
-| IRType.uint16 => emit "lean_ctor_get_uint16"
-| IRType.uint32 => emit "lean_ctor_get_uint32"
-| IRType.uint64 => emit "lean_ctor_get_uint64"
-| _             => throw "invalid instruction";
-emit "("; emit x; emit ", "; emitOffset n offset; emitLn ");"
+do emitLhs z;
+   match t with
+   | IRType.float  => throw "floats are not supported yet"
+   | IRType.uint8  => emit "lean_ctor_get_uint8"
+   | IRType.uint16 => emit "lean_ctor_get_uint16"
+   | IRType.uint32 => emit "lean_ctor_get_uint32"
+   | IRType.uint64 => emit "lean_ctor_get_uint64"
+   | _             => throw "invalid instruction";
+   emit "("; emit x; emit ", "; emitOffset n offset; emitLn ");"
 
 def toStringArgs (ys : Array Arg) : List String :=
 ys.toList.map argToCString
 
 def emitFullApp (z : VarId) (f : FunId) (ys : Array Arg) : M Unit :=
-do
-emitLhs z;
-decl ← getDecl f;
-match decl with
-| Decl.extern _ _ _ extData =>
-  match mkExternCall extData `c (toStringArgs ys) with
-  | some c => emit c *> emitLn ";"
-  | none   => throw ("failed to emit extern application '" ++ toString f ++ "'")
-| _ => do emitCName f; when (ys.size > 0) (do emit "("; emitArgs ys; emit ")"); emitLn ";"
+do emitLhs z;
+   decl ← getDecl f;
+   match decl with
+   | Decl.extern _ _ _ extData =>
+     match mkExternCall extData `c (toStringArgs ys) with
+     | some c => emit c *> emitLn ";"
+     | none   => throw ("failed to emit extern application '" ++ toString f ++ "'")
+   | _ => do emitCName f; when (ys.size > 0) (do emit "("; emitArgs ys; emit ")"); emitLn ";"
 
 def emitPartialApp (z : VarId) (f : FunId) (ys : Array Arg) : M Unit :=
-do
-decl ← getDecl f;
-let arity := decl.params.size;
-emitLhs z; emit "lean_alloc_closure((void*)("; emitCName f; emit "), "; emit arity; emit ", "; emit ys.size; emitLn ");";
-ys.size.mfor $ fun i => do {
-   let y := ys.get! i;
-   emit "lean_closure_set("; emit z; emit ", "; emit i; emit ", "; emitArg y; emitLn ");"
-}
+do decl ← getDecl f;
+   let arity := decl.params.size;
+   emitLhs z; emit "lean_alloc_closure((void*)("; emitCName f; emit "), "; emit arity; emit ", "; emit ys.size; emitLn ");";
+   ys.size.mfor $ fun i => do {
+     let y := ys.get! i;
+     emit "lean_closure_set("; emit z; emit ", "; emit i; emit ", "; emitArg y; emitLn ");"
+   }
 
 def emitApp (z : VarId) (f : VarId) (ys : Array Arg) : M Unit :=
 if ys.size > closureMaxArgs then do
@@ -449,15 +430,14 @@ def emitBox (z : VarId) (x : VarId) (xType : IRType) : M Unit :=
 do emitLhs z; emitBoxFn xType; emit "("; emit x; emitLn ");"
 
 def emitUnbox (z : VarId) (t : IRType) (x : VarId) : M Unit :=
-do
-emitLhs z;
-match t with
-| IRType.usize  => emit "lean_unbox_usize"
-| IRType.uint32 => emit "lean_unbox_uint32"
-| IRType.uint64 => emit "lean_unbox_uint64"
-| IRType.float  => throw "floats are not supported yet"
-| other         => emit "lean_unbox";
-emit "("; emit x; emitLn ");"
+do emitLhs z;
+   match t with
+   | IRType.usize  => emit "lean_unbox_usize"
+   | IRType.uint32 => emit "lean_unbox_uint32"
+   | IRType.uint64 => emit "lean_unbox_uint64"
+   | IRType.float  => throw "floats are not supported yet"
+   | other         => emit "lean_unbox";
+   emit "("; emit x; emitLn ");"
 
 def emitIsShared (z : VarId) (x : VarId) : M Unit :=
 do emitLhs z; emit "!lean_is_exclusive("; emit x; emitLn ");"
@@ -516,11 +496,10 @@ match v with
 | Expr.lit v          => emitLit z t v
 
 def isTailCall (x : VarId) (v : Expr) (b : FnBody) : M Bool :=
-do
-ctx ← read;
-match v, b with
-| Expr.fap f _, FnBody.ret (Arg.var y) => pure $ f == ctx.mainFn && x == y
-| _, _ => pure false
+do ctx ← read;
+   match v, b with
+   | Expr.fap f _, FnBody.ret (Arg.var y) => pure $ f == ctx.mainFn && x == y
+   | _, _ => pure false
 
 def paramEqArg (p : Param) (x : Arg) : Bool :=
 match x with
@@ -610,40 +589,39 @@ emitJPs emitFnBody b;
 emitLn "}"
 
 def emitDeclAux (d : Decl) : M Unit :=
-do
-env ← getEnv;
-let (vMap, jpMap) := mkVarJPMaps d;
-adaptReader (fun (ctx : Context) => { jpMap := jpMap, .. ctx }) $ do
-unless (hasInitAttr env d.name) $
-  match d with
-  | Decl.fdecl f xs t b => do
-    baseName ← toCName f;
-    emit (toCType t); emit " ";
-    if xs.size > 0 then do {
-      emit baseName;
-      emit "(";
-      if xs.size > closureMaxArgs && isBoxedName d.name then
-        emit "lean_object** _args"
-      else
-        xs.size.mfor $ fun i => do {
-          when (i > 0) (emit ", ");
-          let x := xs.get! i;
-          emit (toCType x.ty); emit " "; emit x.x
-        };
-      emit ")"
-    } else do {
-      emit ("_init_" ++ baseName ++ "()")
-    };
-    emitLn " {";
-    when (xs.size > closureMaxArgs && isBoxedName d.name) $
-      xs.size.mfor $ fun i => do {
-        let x := xs.get! i;
-        emit "lean_object* "; emit x.x; emit " = _args["; emit i; emitLn "];"
-      };
-    emitLn "_start:";
-    adaptReader (fun (ctx : Context) => { mainFn := f, mainParams := xs, .. ctx }) (emitFnBody b);
-    emitLn "}"
-  | _ => pure ()
+do env ← getEnv;
+   let (vMap, jpMap) := mkVarJPMaps d;
+   adaptReader (fun (ctx : Context) => { jpMap := jpMap, .. ctx }) $ do
+   unless (hasInitAttr env d.name) $
+     match d with
+     | Decl.fdecl f xs t b => do
+       baseName ← toCName f;
+       emit (toCType t); emit " ";
+       if xs.size > 0 then do {
+         emit baseName;
+         emit "(";
+         if xs.size > closureMaxArgs && isBoxedName d.name then
+           emit "lean_object** _args"
+         else
+           xs.size.mfor $ fun i => do {
+             when (i > 0) (emit ", ");
+             let x := xs.get! i;
+             emit (toCType x.ty); emit " "; emit x.x
+           };
+         emit ")"
+       } else do {
+         emit ("_init_" ++ baseName ++ "()")
+       };
+       emitLn " {";
+       when (xs.size > closureMaxArgs && isBoxedName d.name) $
+         xs.size.mfor $ fun i => do {
+           let x := xs.get! i;
+           emit "lean_object* "; emit x.x; emit " = _args["; emit i; emitLn "];"
+         };
+       emitLn "_start:";
+       adaptReader (fun (ctx : Context) => { mainFn := f, mainParams := xs, .. ctx }) (emitFnBody b);
+       emitLn "}"
+     | _ => pure ()
 
 def emitDecl (d : Decl) : M Unit :=
 let d := d.normalizeIds;
@@ -652,63 +630,53 @@ catch
   (fun err => throw (err ++ "\ncompiling:\n" ++ toString d))
 
 def emitFns : M Unit :=
-do
-env ← getEnv;
-let decls := getDecls env;
-decls.reverse.mfor emitDecl
+do env ← getEnv;
+   let decls := getDecls env;
+   decls.reverse.mfor emitDecl
 
 def emitDeclInit (d : Decl) : M Unit :=
-do
-env ← getEnv;
-let n := d.name;
-if isIOUnitInitFn env n then do {
-  emit "w = "; emitCName n; emitLn "(w);";
-  emitLn "if (lean_io_result_is_error(w)) return w;"
-} else when (d.params.size == 0) $ do {
-  match getInitFnNameFor env d.name with
-  | some initFn => do {
-    emit "w = "; emitCName initFn; emitLn "(w);";
-    emitLn "if (lean_io_result_is_error(w)) return w;";
-    emitCName n; emitLn " = lean_io_result_get_value(w);"
-  }
-  | _ => do {
-    emitCName n; emit " = "; emitCInitName n; emitLn "();"
-  };
-  when d.resultType.isObj $ do {
-    emit "lean_mark_persistent("; emitCName n; emitLn ");"
-  }
-}
+do env ← getEnv;
+   let n := d.name;
+   if isIOUnitInitFn env n then do {
+     emit "w = "; emitCName n; emitLn "(w);";
+     emitLn "if (lean_io_result_is_error(w)) return w;"
+   } else when (d.params.size == 0) $ do {
+     match getInitFnNameFor env d.name with
+     | some initFn => do {
+       emit "w = "; emitCName initFn; emitLn "(w);";
+       emitLn "if (lean_io_result_is_error(w)) return w;";
+       emitCName n; emitLn " = lean_io_result_get_value(w);"
+       }
+     | _ => do { emitCName n; emit " = "; emitCInitName n; emitLn "();" };
+     when d.resultType.isObj $ do {
+       emit "lean_mark_persistent("; emitCName n; emitLn ");"
+     }
+   }
 
 def emitInitFn : M Unit :=
-do
-env ← getEnv;
-modName ← getModName;
-env.imports.mfor $ fun m => emitLn ("lean_object* initialize_" ++ m.mangle "" ++ "(lean_object*);");
-emitLns [
-    "static bool _G_initialized = false;",
-    "lean_object* initialize_" ++ modName.mangle "" ++ "(lean_object* w) {",
-    "if (_G_initialized) return w;",
-    "_G_initialized = true;",
-    "if (lean_io_result_is_error(w)) return w;"
-];
-env.imports.mfor $ fun m => emitLns [
-  "w = initialize_" ++ m.mangle "" ++ "(w);",
-  "if (lean_io_result_is_error(w)) return w;"
-];
-let decls := getDecls env;
-decls.reverse.mfor emitDeclInit;
-emitLns [
-  "return w;",
-  "}"]
+do env ← getEnv;
+   modName ← getModName;
+   env.imports.mfor $ fun m => emitLn ("lean_object* initialize_" ++ m.mangle "" ++ "(lean_object*);");
+   emitLns [
+     "static bool _G_initialized = false;",
+     "lean_object* initialize_" ++ modName.mangle "" ++ "(lean_object* w) {",
+     "if (_G_initialized) return w;",
+     "_G_initialized = true;",
+     "if (lean_io_result_is_error(w)) return w;"];
+   env.imports.mfor $ fun m => emitLns [
+     "w = initialize_" ++ m.mangle "" ++ "(w);",
+     "if (lean_io_result_is_error(w)) return w;"];
+   let decls := getDecls env;
+   decls.reverse.mfor emitDeclInit;
+   emitLns ["return w;", "}"]
 
 def main : M Unit :=
-do
-emitFileHeader;
-emitFnDecls;
-emitFns;
-emitInitFn;
-emitMainFnIfNeeded;
-emitFileFooter
+do emitFileHeader;
+   emitFnDecls;
+   emitFns;
+   emitInitFn;
+   emitMainFnIfNeeded;
+   emitFileFooter
 
 end EmitC
 
diff --git a/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean b/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean
index fd024c11c7..c7f321be70 100644
--- a/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean
+++ b/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean
@@ -239,24 +239,22 @@ and `z := reuse x ctor_i ws; F` is replaced with
 `set x i ws[i]` operations, and we replace `z` with `x` in `F`
 -/
 def mkFastPath (x y : VarId) (mask : Mask) (b : FnBody) : M FnBody :=
-do
-ctx ← read;
-let b := reuseToSet ctx x y b;
-releaseUnreadFields y mask b
+do ctx ← read;
+   let b := reuseToSet ctx x y b;
+   releaseUnreadFields y mask b
 
 -- Expand `bs; x := reset[n] y; b`
 partial def expand (mainFn : FnBody → Array FnBody → M FnBody)
             (bs : Array FnBody) (x : VarId) (n : Nat) (y : VarId) (b : FnBody) : M FnBody :=
-do
-let bOld := FnBody.vdecl x IRType.object (Expr.reset n y) b;
-let (bs, mask) := eraseProjIncFor n y bs;
-let bSlow      := mkSlowPath x y mask b;
-bFast ← mkFastPath x y mask b;
-/- We only optimize recursively the fast. -/
-bFast ← mainFn bFast Array.empty;
-c ← mkFresh;
-let b := FnBody.vdecl c IRType.uint8 (Expr.isShared y) (mkIf c bSlow bFast);
-pure $ reshape bs b
+do let bOld := FnBody.vdecl x IRType.object (Expr.reset n y) b;
+   let (bs, mask) := eraseProjIncFor n y bs;
+   let bSlow      := mkSlowPath x y mask b;
+   bFast ← mkFastPath x y mask b;
+   /- We only optimize recursively the fast. -/
+   bFast ← mainFn bFast Array.empty;
+   c ← mkFresh;
+   let b := FnBody.vdecl c IRType.uint8 (Expr.isShared y) (mkIf c bSlow bFast);
+   pure $ reshape bs b
 
 partial def searchAndExpand : FnBody → Array FnBody → M FnBody
 | d@(FnBody.vdecl x t (Expr.reset n y) b), bs =>
diff --git a/library/Init/Lean/Elaborator/Basic.lean b/library/Init/Lean/Elaborator/Basic.lean
index 93386be2b6..1da00074c0 100644
--- a/library/Init/Lean/Elaborator/Basic.lean
+++ b/library/Init/Lean/Elaborator/Basic.lean
@@ -192,23 +192,22 @@ The state is initialized using `builtinTermElabTable`.
 The current implementation just uses the bultin elaborators.
 -/
 def mkElabAttribute {σ} [Inhabited σ] (attrName : Name) (kind : String) (builtinTable : IO.Ref σ) : IO (ElabAttribute σ) :=
-do
-ext : PersistentEnvExtension ElabAttributeEntry σ ← registerPersistentEnvExtension {
-  name            := attrName,
-  addImportedFn   := fun es => do
-    table ← builtinTable.get;
-    -- TODO: populate table with `es`
-    pure table,
-  addEntryFn      := fun (s : σ) _ => s,                            -- TODO
-  exportEntriesFn := fun _ => Array.empty,                          -- TODO
-  statsFn         := fun _ => fmt (kind ++ " elaborator attribute") -- TODO
-};
-let attrImpl : AttributeImpl := {
-  name  := attrName,
-  descr := kind ++ " elaborator",
-  add   := fun env decl args persistent => pure env -- TODO
-};
-pure { ext := ext, attr := attrImpl, kind := kind }
+do ext : PersistentEnvExtension ElabAttributeEntry σ ← registerPersistentEnvExtension {
+     name            := attrName,
+     addImportedFn   := fun es => do
+       table ← builtinTable.get;
+       -- TODO: populate table with `es`
+       pure table,
+     addEntryFn      := fun (s : σ) _ => s,                            -- TODO
+     exportEntriesFn := fun _ => Array.empty,                          -- TODO
+     statsFn         := fun _ => fmt (kind ++ " elaborator attribute") -- TODO
+   };
+   let attrImpl : AttributeImpl := {
+     name  := attrName,
+     descr := kind ++ " elaborator",
+     add   := fun env decl args persistent => pure env -- TODO
+   };
+   pure { ext := ext, attr := attrImpl, kind := kind }
 
 abbrev TermElabAttribute := ElabAttribute TermElabTable
 def mkTermElabAttribute : IO TermElabAttribute :=
@@ -437,11 +436,10 @@ def localContext : Elab LocalContext :=
 do scope ← getScope; pure scope.lctx
 
 def mkLocalDecl (userName : Name) (type : Expr) (bi : BinderInfo := BinderInfo.default) : Elab LocalDecl :=
-do
-idx ← mkFreshName;
-modifyGetScope $ fun scope =>
-   let (decl, lctx) := scope.lctx.mkLocalDecl idx userName type bi;
-   (decl, { lctx := lctx, .. scope })
+do idx ← mkFreshName;
+   modifyGetScope $ fun scope =>
+      let (decl, lctx) := scope.lctx.mkLocalDecl idx userName type bi;
+      (decl, { lctx := lctx, .. scope })
 
 def mkLambda (xs : Array Expr) (b : Expr) : Elab Expr :=
 do lctx ← localContext; pure $ lctx.mkLambda xs b
@@ -452,11 +450,10 @@ do lctx ← localContext; pure $ lctx.mkForall xs b
 def anonymousInstNamePrefix := `_inst
 
 def mkAnonymousInstName : Elab Name :=
-do
-scope ← getScope;
-let n := anonymousInstNamePrefix.appendIndexAfter scope.nextInstIdx;
-modifyScope $ fun scope => { nextInstIdx := scope.nextInstIdx + 1, .. scope };
-pure n
+do scope ← getScope;
+   let n := anonymousInstNamePrefix.appendIndexAfter scope.nextInstIdx;
+   modifyScope $ fun scope => { nextInstIdx := scope.nextInstIdx + 1, .. scope };
+   pure n
 
 def rootNamespace := `_root_
 
@@ -493,11 +490,10 @@ do s ← get;
        | none   => throw (ElabException.other ("unknown namespace '" ++ toString n ++ "'"))
 
 @[inline] def withNewScope {α} (x : Elab α) : Elab α :=
-do
-modify $ fun s => { scopes := s.scopes.head! :: s.scopes, .. s };
-a ← x;
-modify $ fun s => { scopes := s.scopes.tail!, .. s};
-pure a
+do modify $ fun s => { scopes := s.scopes.head! :: s.scopes, .. s };
+   a ← x;
+   modify $ fun s => { scopes := s.scopes.tail!, .. s};
+   pure a
 
 @[inline] def withInPattern {α} (x : Elab α) : Elab α :=
 withNewScope $ do
diff --git a/library/Init/Lean/Elaborator/Command.lean b/library/Init/Lean/Elaborator/Command.lean
index 59a9150893..73e901398a 100644
--- a/library/Init/Lean/Elaborator/Command.lean
+++ b/library/Init/Lean/Elaborator/Command.lean
@@ -98,50 +98,47 @@ nss.mforArgs $ fun ns => do
   addOpenDecl (OpenDecl.simple ns [])
 
 def elabOpenOnly (n : SyntaxNode) : Elab Unit :=
-do
-let ns  := n.getIdAt 0;
-ns ← resolveNamespace ns;
-let ids := n.getArg 2;
-ids.mforArgs $ fun idStx => do
-  let id := idStx.getId;
-  let declName := ns ++ id;
-  env ← getEnv;
-  if env.contains declName then
-    addOpenDecl (OpenDecl.explicit id declName)
-  else
-    logUnknownDecl idStx declName
+do let ns  := n.getIdAt 0;
+   ns ← resolveNamespace ns;
+   let ids := n.getArg 2;
+   ids.mforArgs $ fun idStx => do
+     let id := idStx.getId;
+     let declName := ns ++ id;
+     env ← getEnv;
+     if env.contains declName then
+       addOpenDecl (OpenDecl.explicit id declName)
+     else
+       logUnknownDecl idStx declName
 
 def elabOpenHiding (n : SyntaxNode) : Elab Unit :=
-do
-let ns := n.getIdAt 0;
-ns ← resolveNamespace ns;
-let idsStx := n.getArg 2;
-env ← getEnv;
-ids : List Name ← idsStx.mfoldArgs (fun idStx ids => do
-  let id := idStx.getId;
-  let declName := ns ++ id;
-  if env.contains declName then
-    pure (id::ids)
-  else do
-    logUnknownDecl idStx declName;
-    pure ids)
-  [];
-addOpenDecl (OpenDecl.simple ns ids)
+do let ns := n.getIdAt 0;
+   ns ← resolveNamespace ns;
+   let idsStx := n.getArg 2;
+   env ← getEnv;
+   ids : List Name ← idsStx.mfoldArgs (fun idStx ids => do
+     let id := idStx.getId;
+     let declName := ns ++ id;
+     if env.contains declName then
+       pure (id::ids)
+     else do
+       logUnknownDecl idStx declName;
+       pure ids)
+     [];
+   addOpenDecl (OpenDecl.simple ns ids)
 
 def elabOpenRenaming (n : SyntaxNode) : Elab Unit :=
-do
-let ns := n.getIdAt 0;
-ns ← resolveNamespace ns;
-let rs := (n.getArg 2);
-rs.mforSepArgs $ fun stx => do
-  let fromId   := stx.getIdAt 0;
-  let toId     := stx.getIdAt 2;
-  let declName := ns ++ fromId;
-  env ← getEnv;
-  if env.contains declName then
-    addOpenDecl (OpenDecl.explicit toId declName)
-  else
-    logUnknownDecl stx declName
+do let ns := n.getIdAt 0;
+   ns ← resolveNamespace ns;
+   let rs := (n.getArg 2);
+   rs.mforSepArgs $ fun stx => do
+     let fromId   := stx.getIdAt 0;
+     let toId     := stx.getIdAt 2;
+     let declName := ns ++ fromId;
+     env ← getEnv;
+     if env.contains declName then
+       addOpenDecl (OpenDecl.explicit toId declName)
+     else
+       logUnknownDecl stx declName
 
 @[builtinCommandElab «open»] def elabOpen : CommandElab :=
 fun n => do
@@ -157,13 +154,12 @@ fun n => do
     elabOpenRenaming body
 
 def addUniverse (idStx : Syntax) : Elab Unit :=
-do
-let id := idStx.getId;
-univs ← getUniverses;
-if univs.elem id then
-  logError idStx ("a universe named '" ++ toString id ++ "' has already been declared in this Scope")
-else
-  modifyScope $ fun scope => { univs := id :: scope.univs, .. scope }
+do let id := idStx.getId;
+   univs ← getUniverses;
+   if univs.elem id then
+     logError idStx ("a universe named '" ++ toString id ++ "' has already been declared in this Scope")
+   else
+     modifyScope $ fun scope => { univs := id :: scope.univs, .. scope }
 
 @[builtinCommandElab «universe»] def elabUniverse : CommandElab :=
 fun n => do
diff --git a/library/Init/Lean/Elaborator/PreTerm.lean b/library/Init/Lean/Elaborator/PreTerm.lean
index 9ebcd3a10c..b164fe23ad 100644
--- a/library/Init/Lean/Elaborator/PreTerm.lean
+++ b/library/Init/Lean/Elaborator/PreTerm.lean
@@ -201,19 +201,18 @@ fun n => do
     logErrorAndThrow n.val ("unknown identifier '" ++ toString id ++ "'")
 
 def oldElaborate (stx : Syntax Expr) (expectedType : Option Expr := none) : Elab Expr :=
-do
-  p ← toPreTerm stx;
-  scope ← getScope;
-  s ← get;
-  match oldElaborateAux s.env scope.options s.mctx scope.lctx (mkPreTypeAscriptionIfSome p expectedType) with
-  | Except.error (some pos, fmt) => do
-    ctx ← read;
-    logMessage { fileName := ctx.fileName, pos := pos, text := fmt.pretty scope.options };
-    throw ElabException.silent
-  | Except.error (none, fmt)     => logErrorAndThrow stx (fmt.pretty scope.options)
-  | Except.ok (env, mctx, e)     => do
-    modify $ fun s => { env := env, mctx := mctx, .. s };
-    pure e
+do p ← toPreTerm stx;
+   scope ← getScope;
+   s ← get;
+   match oldElaborateAux s.env scope.options s.mctx scope.lctx (mkPreTypeAscriptionIfSome p expectedType) with
+     | Except.error (some pos, fmt) => do
+       ctx ← read;
+       logMessage { fileName := ctx.fileName, pos := pos, text := fmt.pretty scope.options };
+       throw ElabException.silent
+     | Except.error (none, fmt)     => logErrorAndThrow stx (fmt.pretty scope.options)
+     | Except.ok (env, mctx, e)     => do
+       modify $ fun s => { env := env, mctx := mctx, .. s };
+       pure e
 
 end Elab
 end Lean
diff --git a/library/Init/Lean/Parser/Module.lean b/library/Init/Lean/Parser/Module.lean
index 2809e80f1d..d5490c6690 100644
--- a/library/Init/Lean/Parser/Module.lean
+++ b/library/Init/Lean/Parser/Module.lean
@@ -120,12 +120,11 @@ partial def parseFileAux (env : Environment) (ctx : ParserContextCore) : ModuleP
       parseFileAux state msgs (stxs.push stx)
 
 def parseFile (env : Environment) (fname : String) : IO Syntax :=
-do
-fname ← IO.realPath fname;
-contents ← IO.readTextFile fname;
-let ctx := mkParserContextCore env contents fname;
-let (stx, state, messages) := parseHeader env ctx;
-parseFileAux env ctx state messages #[stx]
+do fname ← IO.realPath fname;
+   contents ← IO.readTextFile fname;
+   let ctx := mkParserContextCore env contents fname;
+   let (stx, state, messages) := parseHeader env ctx;
+   parseFileAux env ctx state messages #[stx]
 
 end Parser
 end Lean
diff --git a/library/Init/Lean/Parser/Parser.lean b/library/Init/Lean/Parser/Parser.lean
index 61d93984b7..c2c5ecfbd6 100644
--- a/library/Init/Lean/Parser/Parser.lean
+++ b/library/Init/Lean/Parser/Parser.lean
@@ -1346,20 +1346,19 @@ instance TokenTableAttribute.inhabited : Inhabited TokenTableAttribute := ⟨{ a
 section
 set_option compiler.extract_closed false
 def mkTokenTableAttribute : IO TokenTableAttribute :=
-do
-ext : PersistentEnvExtension TokenConfig TokenTable ← registerPersistentEnvExtension {
-  name            := `_tokens_,
-  addImportedFn   := fun es => mkImportedTokenTable es,
-  addEntryFn      := fun (s : TokenTable) _ => s,         -- TODO
-  exportEntriesFn := fun _ => Array.empty,                -- TODO
-  statsFn         := fun _ => fmt "token table attribute" -- TODO
-};
-let attrImpl : AttributeImpl := {
-  name  := `_tokens_,
-  descr := "internal token table attribute",
-  add   := fun env decl args persistent => pure env -- TODO
-};
-pure { ext := ext, attr := attrImpl }
+do ext : PersistentEnvExtension TokenConfig TokenTable ← registerPersistentEnvExtension {
+     name            := `_tokens_,
+     addImportedFn   := fun es => mkImportedTokenTable es,
+     addEntryFn      := fun (s : TokenTable) _ => s,         -- TODO
+     exportEntriesFn := fun _ => Array.empty,                -- TODO
+     statsFn         := fun _ => fmt "token table attribute" -- TODO
+   };
+   let attrImpl : AttributeImpl := {
+     name  := `_tokens_,
+     descr := "internal token table attribute",
+     add   := fun env decl args persistent => pure env -- TODO
+   };
+   pure { ext := ext, attr := attrImpl }
 end
 
 @[init mkTokenTableAttribute]
@@ -1512,25 +1511,24 @@ We still need to:
 - Add support for scoped parser extensions.
 -/
 def registerParserAttribute (attrName : Name) (kind : String) (descr : String) (builtinTable : Option (IO.Ref ParsingTables) := none) : IO ParserAttribute :=
-do
-ext : PersistentEnvExtension ParserAttributeEntry ParsingTables ← registerPersistentEnvExtension {
-  name            := attrName,
-  addImportedFn   := fun es => do
-    table ← match builtinTable with
-    | some table => table.get
-    | none       => pure {};
+do ext : PersistentEnvExtension ParserAttributeEntry ParsingTables ← registerPersistentEnvExtension {
+     name            := attrName,
+     addImportedFn   := fun es => do
+       table ← match builtinTable with
+       | some table => table.get
+       | none       => pure {};
     -- TODO: populate table with `es`
-    pure table,
-  addEntryFn      := fun (s : ParsingTables) _ => s, -- TODO
-  exportEntriesFn := fun _ => Array.empty,           -- TODO
-  statsFn         := fun _ => fmt "parser attribute" -- TODO
-};
-let attrImpl : AttributeImpl := {
-  name  := attrName,
-  descr := descr,
-  add   := fun env decl args persistent => pure env -- TODO
-};
-pure { ext := ext, attr := attrImpl, kind := kind }
+       pure table,
+     addEntryFn      := fun (s : ParsingTables) _ => s, -- TODO
+     exportEntriesFn := fun _ => Array.empty,           -- TODO
+     statsFn         := fun _ => fmt "parser attribute" -- TODO
+   };
+   let attrImpl : AttributeImpl := {
+     name  := attrName,
+     descr := descr,
+     add   := fun env decl args persistent => pure env -- TODO
+   };
+   pure { ext := ext, attr := attrImpl, kind := kind }
 
 namespace ParserAttribute