From fd9e9057c6a6956205faadcefd77a5ee1852f25f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 24 Oct 2020 15:55:36 -0700
Subject: [PATCH] chore: update stage0

---
 stage0/src/Lean/Elab/MutualDef.lean | 607 ++++++++++++++--------------
 stage0/src/Std/Data/RBMap.lean      | 342 ++++++++--------
 stage0/src/Std/Data/RBTree.lean     |  72 ++--
 stage0/stdlib/Lean/Elab/MutualDef.c |  18 -
 stage0/stdlib/Std/Data/RBMap.c      |  84 ++--
 stage0/stdlib/Std/Data/RBTree.c     |  36 +-
 6 files changed, 564 insertions(+), 595 deletions(-)

diff --git a/stage0/src/Lean/Elab/MutualDef.lean b/stage0/src/Lean/Elab/MutualDef.lean
index 83db728e1a..f5e89faf63 100644
--- a/stage0/src/Lean/Elab/MutualDef.lean
+++ b/stage0/src/Lean/Elab/MutualDef.lean
@@ -14,112 +14,112 @@ namespace Lean.Elab
 
 /- DefView after elaborating the header. -/
 structure DefViewElabHeader :=
-(ref           : Syntax)
-(modifiers     : Modifiers)
-(kind          : DefKind)
-(shortDeclName : Name)
-(declName      : Name)
-(levelNames    : List Name)
-(numParams     : Nat)
-(type          : Expr) -- including the parameters
-(valueStx      : Syntax)
+  (ref           : Syntax)
+  (modifiers     : Modifiers)
+  (kind          : DefKind)
+  (shortDeclName : Name)
+  (declName      : Name)
+  (levelNames    : List Name)
+  (numParams     : Nat)
+  (type          : Expr) -- including the parameters
+  (valueStx      : Syntax)
 
 instance : Inhabited DefViewElabHeader :=
-⟨⟨arbitrary _, {}, DefKind.«def», arbitrary _, arbitrary _, [], 0, arbitrary _, arbitrary _⟩⟩
+  ⟨⟨arbitrary _, {}, DefKind.«def», arbitrary _, arbitrary _, [], 0, arbitrary _, arbitrary _⟩⟩
 
 namespace Term
 
 open Meta
 
 private def checkModifiers (m₁ m₂ : Modifiers) : TermElabM Unit := do
-unless m₁.isUnsafe == m₂.isUnsafe do
-  throwError "cannot mix unsafe and safe definitions"
-unless m₁.isNoncomputable == m₂.isNoncomputable do
-  throwError "cannot mix computable and non-computable definitions"
-unless m₁.isPartial == m₂.isPartial do
-  throwError "cannot mix partial and non-partial definitions"
+  unless m₁.isUnsafe == m₂.isUnsafe do
+    throwError "cannot mix unsafe and safe definitions"
+  unless m₁.isNoncomputable == m₂.isNoncomputable do
+    throwError "cannot mix computable and non-computable definitions"
+  unless m₁.isPartial == m₂.isPartial do
+    throwError "cannot mix partial and non-partial definitions"
 
 private def checkKinds (k₁ k₂ : DefKind) : TermElabM Unit := do
-unless k₁.isExample == k₂.isExample do
-  throwError "cannot mix examples and definitions" -- Reason: we should discard examples
-unless k₁.isTheorem == k₂.isTheorem do
-  throwError "cannot mix theorems and definitions" -- Reason: we will eventually elaborate theorems in `Task`s.
+  unless k₁.isExample == k₂.isExample do
+    throwError "cannot mix examples and definitions" -- Reason: we should discard examples
+  unless k₁.isTheorem == k₂.isTheorem do
+    throwError "cannot mix theorems and definitions" -- Reason: we will eventually elaborate theorems in `Task`s.
 
 private def check (prevHeaders : Array DefViewElabHeader) (newHeader : DefViewElabHeader) : TermElabM Unit := do
-if newHeader.kind.isTheorem && newHeader.modifiers.isUnsafe then
-  throwError "'unsafe' theorems are not allowed"
-if newHeader.kind.isTheorem && newHeader.modifiers.isPartial then
-  throwError "'partial' theorems are not allowed, 'partial' is a code generation directive"
-if newHeader.kind.isTheorem && newHeader.modifiers.isNoncomputable then
-  throwError "'theorem' subsumes 'noncomputable', code is not generated for theorems"
-if newHeader.modifiers.isNoncomputable && newHeader.modifiers.isUnsafe then
-  throwError "'noncomputable unsafe' is not allowed"
-if newHeader.modifiers.isNoncomputable && newHeader.modifiers.isPartial then
-  throwError "'noncomputable partial' is not allowed"
-if newHeader.modifiers.isPartial && newHeader.modifiers.isUnsafe then
-  throwError "'unsafe' subsumes 'partial'"
-if h : 0 < prevHeaders.size then
-  let firstHeader := prevHeaders.get ⟨0, h⟩
-  try
-    unless newHeader.levelNames == firstHeader.levelNames do
-      throwError "universe parameters mismatch"
-    checkModifiers newHeader.modifiers firstHeader.modifiers
-    checkKinds newHeader.kind firstHeader.kind
-  catch
-     | Exception.error ref msg => throw (Exception.error ref msg!"invalid mutually recursive definitions, {msg}")
-     | ex => throw ex
-else
-  pure ()
+  if newHeader.kind.isTheorem && newHeader.modifiers.isUnsafe then
+    throwError "'unsafe' theorems are not allowed"
+  if newHeader.kind.isTheorem && newHeader.modifiers.isPartial then
+    throwError "'partial' theorems are not allowed, 'partial' is a code generation directive"
+  if newHeader.kind.isTheorem && newHeader.modifiers.isNoncomputable then
+    throwError "'theorem' subsumes 'noncomputable', code is not generated for theorems"
+  if newHeader.modifiers.isNoncomputable && newHeader.modifiers.isUnsafe then
+    throwError "'noncomputable unsafe' is not allowed"
+  if newHeader.modifiers.isNoncomputable && newHeader.modifiers.isPartial then
+    throwError "'noncomputable partial' is not allowed"
+  if newHeader.modifiers.isPartial && newHeader.modifiers.isUnsafe then
+    throwError "'unsafe' subsumes 'partial'"
+  if h : 0 < prevHeaders.size then
+    let firstHeader := prevHeaders.get ⟨0, h⟩
+    try
+      unless newHeader.levelNames == firstHeader.levelNames do
+        throwError "universe parameters mismatch"
+      checkModifiers newHeader.modifiers firstHeader.modifiers
+      checkKinds newHeader.kind firstHeader.kind
+    catch
+       | Exception.error ref msg => throw (Exception.error ref msg!"invalid mutually recursive definitions, {msg}")
+       | ex => throw ex
+  else
+    pure ()
 
 private def registerFailedToInferDefTypeInfo (type : Expr) (ref : Syntax) : TermElabM Unit :=
-registerCustomErrorIfMVar type ref "failed to infer definition type"
+  registerCustomErrorIfMVar type ref "failed to infer definition type"
 
 private def elabFunType (ref : Syntax) (xs : Array Expr) (view : DefView) : TermElabM Expr := do
-match view.type? with
-| some typeStx =>
-  let type ← elabType typeStx
-  synthesizeSyntheticMVarsNoPostponing
-  let type ← instantiateMVars type
-  registerFailedToInferDefTypeInfo type typeStx
-  mkForallFVars xs type
-| none =>
-  let hole := mkHole ref
-  let type ← elabType hole
-  registerFailedToInferDefTypeInfo type ref
-  mkForallFVars xs type
+  match view.type? with
+  | some typeStx =>
+    let type ← elabType typeStx
+    synthesizeSyntheticMVarsNoPostponing
+    let type ← instantiateMVars type
+    registerFailedToInferDefTypeInfo type typeStx
+    mkForallFVars xs type
+  | none =>
+    let hole := mkHole ref
+    let type ← elabType hole
+    registerFailedToInferDefTypeInfo type ref
+    mkForallFVars xs type
 
 private def elabHeaders (views : Array DefView) : TermElabM (Array DefViewElabHeader) := do
-let headers := #[]
-for view in views do
-  let newHeader ← withRef view.ref do
-    let ⟨shortDeclName, declName, levelNames⟩ ← expandDeclId (← getCurrNamespace) (← getLevelNames) view.declId view.modifiers
-    applyAttributesAt declName view.modifiers.attrs AttributeApplicationTime.beforeElaboration
-    withLevelNames levelNames $ elabBinders view.binders.getArgs fun xs => do
-      let refForElabFunType := view.value
-      let type ← elabFunType refForElabFunType xs view
-      let newHeader := {
-        ref           := view.ref,
-        modifiers     := view.modifiers,
-        kind          := view.kind,
-        shortDeclName := shortDeclName,
-        declName      := declName,
-        levelNames    := levelNames,
-        numParams     := xs.size,
-        type          := type,
-        valueStx      := view.value : DefViewElabHeader }
-      check headers newHeader
-      pure newHeader
-  headers := headers.push newHeader
-pure headers
+  let headers := #[]
+  for view in views do
+    let newHeader ← withRef view.ref do
+      let ⟨shortDeclName, declName, levelNames⟩ ← expandDeclId (← getCurrNamespace) (← getLevelNames) view.declId view.modifiers
+      applyAttributesAt declName view.modifiers.attrs AttributeApplicationTime.beforeElaboration
+      withLevelNames levelNames $ elabBinders view.binders.getArgs fun xs => do
+        let refForElabFunType := view.value
+        let type ← elabFunType refForElabFunType xs view
+        let newHeader := {
+          ref           := view.ref,
+          modifiers     := view.modifiers,
+          kind          := view.kind,
+          shortDeclName := shortDeclName,
+          declName      := declName,
+          levelNames    := levelNames,
+          numParams     := xs.size,
+          type          := type,
+          valueStx      := view.value : DefViewElabHeader }
+        check headers newHeader
+        pure newHeader
+    headers := headers.push newHeader
+  pure headers
 
 private partial def withFunLocalDecls {α} (headers : Array DefViewElabHeader) (k : Array Expr → TermElabM α) : TermElabM α :=
-let rec loop (i : Nat) (fvars : Array Expr) := do
-  if h : i < headers.size then
-    let header := headers.get ⟨i, h⟩
-    withLocalDecl header.shortDeclName BinderInfo.auxDecl header.type fun fvar => loop (i+1) (fvars.push fvar)
-  else
-    k fvars
-loop 0 #[]
+  let rec loop (i : Nat) (fvars : Array Expr) := do
+    if h : i < headers.size then
+      let header := headers.get ⟨i, h⟩
+      withLocalDecl header.shortDeclName BinderInfo.auxDecl header.type fun fvar => loop (i+1) (fvars.push fvar)
+    else
+      k fvars
+  loop 0 #[]
 
 /-
 Recall that
@@ -134,72 +134,72 @@ def declVal          := declValSimple <|> declValEqns
 ```
 -/
 private def declValToTerm (declVal : Syntax) : MacroM Syntax :=
-if declVal.isOfKind `Lean.Parser.Command.declValSimple then
-  pure declVal[1]
-else if declVal.isOfKind `Lean.Parser.Command.declValEqns then
-  expandMatchAltsIntoMatch declVal declVal[0]
-else
-  Macro.throwError declVal "unexpected definition value"
+  if declVal.isOfKind `Lean.Parser.Command.declValSimple then
+    pure declVal[1]
+  else if declVal.isOfKind `Lean.Parser.Command.declValEqns then
+    expandMatchAltsIntoMatch declVal declVal[0]
+  else
+    Macro.throwError declVal "unexpected definition value"
 
 private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array Expr) :=
-headers.mapM fun header => withDeclName header.declName $ withLevelNames header.levelNames do
-  let valStx ← liftMacroM $ declValToTerm header.valueStx
-  forallBoundedTelescope header.type header.numParams fun xs type => do
-    let val ← elabTermEnsuringType valStx type
-    mkLambdaFVars xs val
+  headers.mapM fun header => withDeclName header.declName $ withLevelNames header.levelNames do
+    let valStx ← liftMacroM $ declValToTerm header.valueStx
+    forallBoundedTelescope header.type header.numParams fun xs type => do
+      let val ← elabTermEnsuringType valStx type
+      mkLambdaFVars xs val
 
 private def collectUsed (headers : Array DefViewElabHeader) (values : Array Expr) (toLift : List LetRecToLift)
     : StateRefT CollectFVars.State TermElabM Unit := do
-headers.forM fun header => collectUsedFVars header.type
-values.forM collectUsedFVars
-toLift.forM fun letRecToLift => do
-  collectUsedFVars letRecToLift.type
-  collectUsedFVars letRecToLift.val
+  headers.forM fun header => collectUsedFVars header.type
+  values.forM collectUsedFVars
+  toLift.forM fun letRecToLift => do
+    collectUsedFVars letRecToLift.type
+    collectUsedFVars letRecToLift.val
 
 private def removeUnusedVars (vars : Array Expr) (headers : Array DefViewElabHeader) (values : Array Expr) (toLift : List LetRecToLift)
     : TermElabM (LocalContext × LocalInstances × Array Expr) := do
-let (_, used) ← (collectUsed headers values toLift).run {}
-removeUnused vars used
+  let (_, used) ← (collectUsed headers values toLift).run {}
+  removeUnused vars used
 
 private def withUsedWhen {α} (vars : Array Expr) (headers : Array DefViewElabHeader) (values : Array Expr) (toLift : List LetRecToLift)
     (cond : Bool) (k : Array Expr → TermElabM α) : TermElabM α := do
-if cond then
- let (lctx, localInsts, vars) ← removeUnusedVars vars headers values toLift
- withLCtx lctx localInsts $ k vars
-else
- k vars
+  if cond then
+   let (lctx, localInsts, vars) ← removeUnusedVars vars headers values toLift
+   withLCtx lctx localInsts $ k vars
+  else
+   k vars
 
 private def isExample (views : Array DefView) : Bool :=
-views.any (·.kind.isExample)
+  views.any (·.kind.isExample)
 
 private def isTheorem (views : Array DefView) : Bool :=
-views.any (·.kind.isTheorem)
+  views.any (·.kind.isTheorem)
 
 private def instantiateMVarsAtHeader (header : DefViewElabHeader) : TermElabM DefViewElabHeader := do
-let type ← instantiateMVars header.type
-pure { header with type := type }
+  let type ← instantiateMVars header.type
+  pure { header with type := type }
 
 private def instantiateMVarsAtLetRecToLift (toLift : LetRecToLift) : TermElabM LetRecToLift := do
-let type ← instantiateMVars toLift.type
-let val ← instantiateMVars toLift.val
-pure { toLift with type := type, val := val }
+  let type ← instantiateMVars toLift.type
+  let val ← instantiateMVars toLift.val
+  pure { toLift with type := type, val := val }
 
 private def typeHasRecFun (type : Expr) (funFVars : Array Expr) (letRecsToLift : List LetRecToLift) : Option FVarId :=
-let occ? := type.find? fun e => match e with
-  | Expr.fvar fvarId _ => funFVars.contains e || letRecsToLift.any fun toLift => toLift.fvarId == fvarId
-  | _ => false
-match occ? with
-| some (Expr.fvar fvarId _) => some fvarId
-| _ => none
+  let occ? := type.find? fun e => match e with
+    | Expr.fvar fvarId _ => funFVars.contains e || letRecsToLift.any fun toLift => toLift.fvarId == fvarId
+    | _ => false
+  match occ? with
+  | some (Expr.fvar fvarId _) => some fvarId
+  | _ => none
 
 private def getFunName (fvarId : FVarId) (letRecsToLift : List LetRecToLift) : TermElabM Name := do
-match (← findLocalDecl? fvarId) with
-| some decl => pure decl.userName
-| none =>
-  /- Recall that the FVarId of nested let-recs are not in the current local context. -/
-  match letRecsToLift.findSome? fun toLift => if toLift.fvarId == fvarId then some toLift.shortDeclName else none with
-  | none   => throwError "unknown function"
-  | some n => pure n
+  match (← findLocalDecl? fvarId) with
+  | some decl => pure decl.userName
+  | none =>
+    /- Recall that the FVarId of nested let-recs are not in the current local context. -/
+    match letRecsToLift.findSome? fun toLift => if toLift.fvarId == fvarId then some toLift.shortDeclName else none with
+    | none   => throwError "unknown function"
+    | some n => pure n
 
 /-
 Ensures that the of let-rec definition types do not contain functions being defined.
@@ -207,12 +207,12 @@ In principle, this test can be improved. We could perform it after we separate t
 However, this extra complication doesn't seem worth it.
 -/
 private def checkLetRecsToLiftTypes (funVars : Array Expr) (letRecsToLift : List LetRecToLift) : TermElabM Unit :=
-letRecsToLift.forM fun toLift =>
-  match typeHasRecFun toLift.type funVars letRecsToLift with
-  | none        => pure ()
-  | some fvarId => do
-    let fnName ← getFunName fvarId letRecsToLift
-    throwErrorAt! toLift.ref "invalid type in 'let rec', it uses '{fnName}' which is being defined simultaneously"
+  letRecsToLift.forM fun toLift =>
+    match typeHasRecFun toLift.type funVars letRecsToLift with
+    | none        => pure ()
+    | some fvarId => do
+      let fnName ← getFunName fvarId letRecsToLift
+      throwErrorAt! toLift.ref "invalid type in 'let rec', it uses '{fnName}' which is being defined simultaneously"
 
 namespace MutualClosure
 
@@ -266,25 +266,25 @@ Note that `g` is not a free variable at `(let g : B := ?m₂; body)`. We recover
 -/
 private def mkInitialUsedFVarsMap (mctx : MetavarContext) (sectionVars : Array Expr) (mainFVarIds : Array FVarId) (letRecsToLift : List LetRecToLift)
     : UsedFVarsMap := do
-let sectionVarSet := {}
-for var in sectionVars do
-  sectionVarSet := sectionVarSet.insert var.fvarId!
-let usedFVarMap := {}
-for mainFVarId in mainFVarIds do
-  usedFVarMap := usedFVarMap.insert mainFVarId sectionVarSet
-for toLift in letRecsToLift do
-  let state := Lean.collectFVars {} toLift.val
-  let state := Lean.collectFVars state toLift.type
-  let set   := state.fvarSet
-  /- toLift.val may contain metavariables that are placeholders for nested let-recs. We should collect the fvarId
-     for the associated let-rec because we need this information to compute the fixpoint later. -/
-  let mvarIds := (toLift.val.collectMVars {}).result
-  for mvarId in mvarIds do
-    match letRecsToLift.findSome? fun (toLift : LetRecToLift) => if toLift.mvarId == mctx.getDelayedRoot mvarId then some toLift.fvarId else none with
-    | some fvarId => set := set.insert fvarId
-    | none        => pure ()
-  usedFVarMap := usedFVarMap.insert toLift.fvarId set
-pure usedFVarMap
+  let sectionVarSet := {}
+  for var in sectionVars do
+    sectionVarSet := sectionVarSet.insert var.fvarId!
+  let usedFVarMap := {}
+  for mainFVarId in mainFVarIds do
+    usedFVarMap := usedFVarMap.insert mainFVarId sectionVarSet
+  for toLift in letRecsToLift do
+    let state := Lean.collectFVars {} toLift.val
+    let state := Lean.collectFVars state toLift.type
+    let set   := state.fvarSet
+    /- toLift.val may contain metavariables that are placeholders for nested let-recs. We should collect the fvarId
+       for the associated let-rec because we need this information to compute the fixpoint later. -/
+    let mvarIds := (toLift.val.collectMVars {}).result
+    for mvarId in mvarIds do
+      match letRecsToLift.findSome? fun (toLift : LetRecToLift) => if toLift.mvarId == mctx.getDelayedRoot mvarId then some toLift.fvarId else none with
+      | some fvarId => set := set.insert fvarId
+      | none        => pure ()
+    usedFVarMap := usedFVarMap.insert toLift.fvarId set
+  pure usedFVarMap
 
 /-
 The let-recs may invoke each other. Example:
@@ -308,8 +308,8 @@ def g (y z : Nat) : Nat → Nat
 namespace FixPoint
 
 structure State :=
-(usedFVarsMap : UsedFVarsMap := {})
-(modified     : Bool         := false)
+  (usedFVarsMap : UsedFVarsMap := {})
+  (modified     : Bool         := false)
 
 abbrev M := ReaderT (List FVarId) $ StateM State
 
@@ -321,22 +321,19 @@ private def modifyUsedFVars (f : UsedFVarsMap → UsedFVarsMap) : M Unit := modi
 
 -- merge s₂ into s₁
 private def merge (s₁ s₂ : NameSet) : M NameSet :=
-s₂.foldM
-  (fun (s₁ : NameSet) k =>
+  s₂.foldM (init := s₁) fun s₁ k => do
     if s₁.contains k then
       pure s₁
-    else do
+    else
       markModified
-      pure $ s₁.insert k)
-  s₁
+      pure $ s₁.insert k
 
 private def updateUsedVarsOf (fvarId : FVarId) : M Unit := do
-let usedFVarsMap ← getUsedFVarsMap
-match usedFVarsMap.find? fvarId with
-| none         => pure ()
-| some fvarIds =>
-  let fvarIdsNew ← fvarIds.foldM
-    (fun (fvarIdsNew : NameSet) (fvarId' : FVarId) =>
+  let usedFVarsMap ← getUsedFVarsMap
+  match usedFVarsMap.find? fvarId with
+  | none         => pure ()
+  | some fvarIds =>
+    let fvarIdsNew ← fvarIds.foldM (init := fvarIds) fun fvarIdsNew fvarId' =>
       if fvarId == fvarId' then
         pure fvarIdsNew
       else
@@ -345,21 +342,20 @@ match usedFVarsMap.find? fvarId with
           /- We are being sloppy here `otherFVarIds` may contain free variables that are
              not in the context of the let-rec associated with fvarId.
              We filter these out-of-context free variables later. -/
-        | some otherFVarIds => merge fvarIdsNew otherFVarIds)
-    fvarIds
-  modifyUsedFVars fun usedFVars => usedFVars.insert fvarId fvarIdsNew
+        | some otherFVarIds => merge fvarIdsNew otherFVarIds
+    modifyUsedFVars fun usedFVars => usedFVars.insert fvarId fvarIdsNew
 
 private partial def fixpoint : Unit → M Unit
-| _ => do
-  resetModified
-  let letRecFVarIds ← read
-  letRecFVarIds.forM updateUsedVarsOf
-  if (← isModified) then
-    fixpoint ()
+  | _ => do
+    resetModified
+    let letRecFVarIds ← read
+    letRecFVarIds.forM updateUsedVarsOf
+    if (← isModified) then
+      fixpoint ()
 
 def run (letRecFVarIds : List FVarId) (usedFVarsMap : UsedFVarsMap) : UsedFVarsMap :=
-let (_, s) := ((fixpoint ()).run letRecFVarIds).run { usedFVarsMap := usedFVarsMap }
-s.usedFVarsMap
+  let (_, s) := ((fixpoint ()).run letRecFVarIds).run { usedFVarsMap := usedFVarsMap }
+  s.usedFVarsMap
 
 end FixPoint
 
@@ -368,55 +364,51 @@ abbrev FreeVarMap := NameMap (Array FVarId)
 private def mkFreeVarMap
     (mctx : MetavarContext) (sectionVars : Array Expr) (mainFVarIds : Array FVarId)
     (recFVarIds : Array FVarId) (letRecsToLift : List LetRecToLift) : FreeVarMap := do
-let usedFVarsMap  := mkInitialUsedFVarsMap mctx sectionVars mainFVarIds letRecsToLift
-let letRecFVarIds := letRecsToLift.map fun toLift => toLift.fvarId
-let usedFVarsMap  := FixPoint.run letRecFVarIds usedFVarsMap
-let freeVarMap := {}
-for toLift in letRecsToLift do
-  let lctx       := toLift.lctx
-  let fvarIdsSet := (usedFVarsMap.find? toLift.fvarId).get!
-  let fvarIds    := fvarIdsSet.fold
-    (fun (fvarIds : Array FVarId) (fvarId : FVarId) =>
+  let usedFVarsMap  := mkInitialUsedFVarsMap mctx sectionVars mainFVarIds letRecsToLift
+  let letRecFVarIds := letRecsToLift.map fun toLift => toLift.fvarId
+  let usedFVarsMap  := FixPoint.run letRecFVarIds usedFVarsMap
+  let freeVarMap := {}
+  for toLift in letRecsToLift do
+    let lctx       := toLift.lctx
+    let fvarIdsSet := (usedFVarsMap.find? toLift.fvarId).get!
+    let fvarIds    := fvarIdsSet.fold (init := #[]) fun fvarIds fvarId =>
       if lctx.contains fvarId && !recFVarIds.contains fvarId then
         fvarIds.push fvarId
       else
-        fvarIds)
-    #[]
-  freeVarMap := freeVarMap.insert toLift.fvarId fvarIds
-pure freeVarMap
+        fvarIds
+    freeVarMap := freeVarMap.insert toLift.fvarId fvarIds
+  pure freeVarMap
 
 structure ClosureState :=
-(newLocalDecls : Array LocalDecl := #[])
-(localDecls    : Array LocalDecl := #[])
-(newLetDecls   : Array LocalDecl := #[])
-(exprArgs      : Array Expr      := #[])
+  (newLocalDecls : Array LocalDecl := #[])
+  (localDecls    : Array LocalDecl := #[])
+  (newLetDecls   : Array LocalDecl := #[])
+  (exprArgs      : Array Expr      := #[])
 
 private def pickMaxFVar? (lctx : LocalContext) (fvarIds : Array FVarId) : Option FVarId :=
-fvarIds.getMax? fun fvarId₁ fvarId₂ => (lctx.get! fvarId₁).index < (lctx.get! fvarId₂).index
+  fvarIds.getMax? fun fvarId₁ fvarId₂ => (lctx.get! fvarId₁).index < (lctx.get! fvarId₂).index
 
 private def preprocess (e : Expr) : TermElabM Expr := do
-let e ← instantiateMVars e
--- which let-decls are dependent. We say a let-decl is dependent if its lambda abstraction is type incorrect.
-Meta.check e
-pure e
+  let e ← instantiateMVars e
+  -- which let-decls are dependent. We say a let-decl is dependent if its lambda abstraction is type incorrect.
+  Meta.check e
+  pure e
 
 /- Push free variables in `s` to `toProcess` if they are not already there. -/
 private def pushNewVars (toProcess : Array FVarId) (s : CollectFVars.State) : Array FVarId :=
-s.fvarSet.fold
-  (fun (toProcess : Array FVarId) fvarId => if toProcess.contains fvarId then toProcess else toProcess.push fvarId)
-  toProcess
+  s.fvarSet.fold (init := toProcess) fun toProcess fvarId =>
+    if toProcess.contains fvarId then toProcess else toProcess.push fvarId
 
 private def pushLocalDecl (toProcess : Array FVarId) (fvarId : FVarId) (userName : Name) (type : Expr) (bi := BinderInfo.default)
     : StateRefT ClosureState TermElabM (Array FVarId) := do
-let type ← preprocess type
-modify fun s => { s with
-  newLocalDecls := s.newLocalDecls.push $ LocalDecl.cdecl (arbitrary _) fvarId userName type bi,
-  exprArgs      := s.exprArgs.push (mkFVar fvarId)
-}
-pure $ pushNewVars toProcess (collectFVars {} type)
+  let type ← preprocess type
+  modify fun s => { s with
+    newLocalDecls := s.newLocalDecls.push $ LocalDecl.cdecl (arbitrary _) fvarId userName type bi,
+    exprArgs      := s.exprArgs.push (mkFVar fvarId)
+  }
+  pure $ pushNewVars toProcess (collectFVars {} type)
 
-private partial def mkClosureForAux : Array FVarId → StateRefT ClosureState TermElabM Unit
-| toProcess => do
+private partial def mkClosureForAux (toProcess : Array FVarId) : StateRefT ClosureState TermElabM Unit := do
   let lctx ← getLCtx
   match pickMaxFVar? lctx toProcess with
   | none        => pure ()
@@ -448,56 +440,56 @@ private partial def mkClosureForAux : Array FVarId → StateRefT ClosureState Te
         mkClosureForAux (pushNewVars toProcess (collectFVars (collectFVars {} type) val))
 
 private partial def mkClosureFor (freeVars : Array FVarId) (localDecls : Array LocalDecl) : TermElabM ClosureState := do
-let (_, s) ← (mkClosureForAux freeVars).run { localDecls := localDecls }
-pure { s with
-  newLocalDecls := s.newLocalDecls.reverse,
-  newLetDecls   := s.newLetDecls.reverse,
-  exprArgs      := s.exprArgs.reverse }
+  let (_, s) ← (mkClosureForAux freeVars).run { localDecls := localDecls }
+  pure { s with
+    newLocalDecls := s.newLocalDecls.reverse,
+    newLetDecls   := s.newLetDecls.reverse,
+    exprArgs      := s.exprArgs.reverse
+  }
 
 structure LetRecClosure :=
-(localDecls : Array LocalDecl)
-(closed     : Expr) -- expression used to replace occurrences of the let-rec FVarId
-(toLift     : LetRecToLift)
+  (localDecls : Array LocalDecl)
+  (closed     : Expr) -- expression used to replace occurrences of the let-rec FVarId
+  (toLift     : LetRecToLift)
 
 private def mkLetRecClosureFor (toLift : LetRecToLift) (freeVars : Array FVarId) : TermElabM LetRecClosure := do
-let lctx := toLift.lctx
-withLCtx lctx toLift.localInstances do
-lambdaTelescope toLift.val fun xs val => do
-  let type ← instantiateForall toLift.type xs
-  let lctx ← getLCtx
-  let s ← mkClosureFor freeVars $ xs.map fun x => lctx.get! x.fvarId!
-  let type := Closure.mkForall s.localDecls $ Closure.mkForall s.newLetDecls type
-  let val  := Closure.mkLambda s.localDecls $ Closure.mkLambda s.newLetDecls val
-  let c    := mkAppN (Lean.mkConst toLift.declName) s.exprArgs
-  assignExprMVar toLift.mvarId c
-  pure ⟨s.newLocalDecls, c, { toLift with val := val, type := type }⟩
+  let lctx := toLift.lctx
+  withLCtx lctx toLift.localInstances do
+  lambdaTelescope toLift.val fun xs val => do
+    let type ← instantiateForall toLift.type xs
+    let lctx ← getLCtx
+    let s ← mkClosureFor freeVars $ xs.map fun x => lctx.get! x.fvarId!
+    let type := Closure.mkForall s.localDecls $ Closure.mkForall s.newLetDecls type
+    let val  := Closure.mkLambda s.localDecls $ Closure.mkLambda s.newLetDecls val
+    let c    := mkAppN (Lean.mkConst toLift.declName) s.exprArgs
+    assignExprMVar toLift.mvarId c
+    pure ⟨s.newLocalDecls, c, { toLift with val := val, type := type }⟩
 
 private def mkLetRecClosures (letRecsToLift : List LetRecToLift) (freeVarMap : FreeVarMap) : TermElabM (List LetRecClosure) :=
-letRecsToLift.mapM fun toLift => mkLetRecClosureFor toLift (freeVarMap.find? toLift.fvarId).get!
+  letRecsToLift.mapM fun toLift => mkLetRecClosureFor toLift (freeVarMap.find? toLift.fvarId).get!
 
 /- Mapping from FVarId of mutually recursive functions being defined to "closure" expression. -/
 abbrev Replacement := NameMap Expr
 
 def insertReplacementForMainFns (r : Replacement) (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mainFVars : Array Expr) : Replacement :=
-mainFVars.size.fold
-  (fun i (r : Replacement) =>
-    r.insert (mainFVars.get! i).fvarId! (mkAppN (Lean.mkConst (mainHeaders.get! i).declName) sectionVars))
-  r
+  mainFVars.size.fold (init := r) fun i r =>
+    r.insert (mainFVars.get! i).fvarId! (mkAppN (Lean.mkConst (mainHeaders.get! i).declName) sectionVars)
+
 
 def insertReplacementForLetRecs (r : Replacement) (letRecClosures : List LetRecClosure) : Replacement :=
-letRecClosures.foldl (fun (r : Replacement) c => r.insert c.toLift.fvarId c.closed) r
+  letRecClosures.foldl (init := r) fun r c =>
+    r.insert c.toLift.fvarId c.closed
 
 def Replacement.apply (r : Replacement) (e : Expr) : Expr :=
-e.replace fun e => match e with
-  | Expr.fvar fvarId _ => match r.find? fvarId with
-    | some c => some c
-    | _      => none
-  | _ => none
+  e.replace fun e => match e with
+    | Expr.fvar fvarId _ => match r.find? fvarId with
+      | some c => some c
+      | _      => none
+    | _ => none
 
 def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mainVals : Array Expr)
     : TermElabM (Array PreDefinition) :=
-mainHeaders.size.foldM
-  (fun i (preDefs : Array PreDefinition) => do
+  mainHeaders.size.foldM (init := preDefs) fun i preDefs => do
     let header := mainHeaders[i]
     let val  ← mkLambdaFVars sectionVars mainVals[i]
     let type ← mkForallFVars sectionVars header.type
@@ -508,12 +500,10 @@ mainHeaders.size.foldM
       modifiers := header.modifiers,
       type      := type,
       value     := val
-    })
-  preDefs
+    }
 
 def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClosure) (kind : DefKind) (modifiers : Modifiers) : Array PreDefinition :=
-letRecClosures.foldl
-  (fun (preDefs : Array PreDefinition) (c : LetRecClosure) =>
+  letRecClosures.foldl (init := preDefs) fun preDefs c =>
     let type := Closure.mkForall c.localDecls c.toLift.type
     let val  := Closure.mkLambda c.localDecls c.toLift.val
     preDefs.push {
@@ -523,17 +513,17 @@ letRecClosures.foldl
       modifiers := { modifiers with attrs := c.toLift.attrs },
       type      := type,
       value     := val
-    })
-  preDefs
+    }
 
 def getKindForLetRecs (mainHeaders : Array DefViewElabHeader) : DefKind :=
-if mainHeaders.any fun h => h.kind.isTheorem then DefKind.«theorem»
-else DefKind.«def»
+  if mainHeaders.any fun h => h.kind.isTheorem then DefKind.«theorem»
+  else DefKind.«def»
 
-def getModifiersForLetRecs (mainHeaders : Array DefViewElabHeader) : Modifiers :=
-{ isNoncomputable := mainHeaders.any fun h => h.modifiers.isNoncomputable,
+def getModifiersForLetRecs (mainHeaders : Array DefViewElabHeader) : Modifiers := {
+  isNoncomputable := mainHeaders.any fun h => h.modifiers.isNoncomputable,
   isPartial       := mainHeaders.any fun h => h.modifiers.isPartial,
-  isUnsafe        := mainHeaders.any fun h => h.modifiers.isUnsafe }
+  isUnsafe        := mainHeaders.any fun h => h.modifiers.isUnsafe
+}
 
 /-
 - `sectionVars`:   The section variables used in the `mutual` block.
@@ -544,71 +534,70 @@ def getModifiersForLetRecs (mainHeaders : Array DefViewElabHeader) : Modifiers :
 -/
 def main (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mainFVars : Array Expr) (mainVals : Array Expr) (letRecsToLift : List LetRecToLift)
     : TermElabM (Array PreDefinition) := do
--- Store in recFVarIds the fvarId of every function being defined by the mutual block.
-let mainFVarIds := mainFVars.map Expr.fvarId!
-let recFVarIds  := (letRecsToLift.toArray.map fun toLift => toLift.fvarId) ++ mainFVarIds
--- Compute the set of free variables (excluding `recFVarIds`) for each let-rec.
-let mctx ← getMCtx
-let freeVarMap := mkFreeVarMap mctx sectionVars mainFVarIds recFVarIds letRecsToLift
-resetZetaFVarIds
-withTrackingZeta do
-  -- By checking `toLift.type` and `toLift.val` we populate `zetaFVarIds`. See comments at `src/Lean/Meta/Closure.lean`.
-  letRecsToLift.forM fun toLift => withLCtx toLift.lctx toLift.localInstances do Meta.check toLift.type; Meta.check toLift.val
-  let letRecClosures ← mkLetRecClosures letRecsToLift freeVarMap
-  -- mkLetRecClosures assign metavariables that were placeholders for the lifted declarations.
-  let mainVals    ← mainVals.mapM instantiateMVars
-  let mainHeaders ← mainHeaders.mapM instantiateMVarsAtHeader
-  let letRecClosures ← letRecClosures.mapM fun closure => do pure { closure with toLift := (← instantiateMVarsAtLetRecToLift closure.toLift) }
-  -- Replace fvarIds for functions being defined with closed terms
-  let r              := insertReplacementForMainFns {} sectionVars mainHeaders mainFVars
-  let r              := insertReplacementForLetRecs r letRecClosures
-  let mainVals       := mainVals.map r.apply
-  let mainHeaders    := mainHeaders.map fun h => { h with type := r.apply h.type }
-  let letRecClosures := letRecClosures.map fun c => { c with toLift := { c.toLift with type := r.apply c.toLift.type, val := r.apply c.toLift.val } }
-  let letRecKind     := getKindForLetRecs mainHeaders
-  let letRecMods     := getModifiersForLetRecs mainHeaders
-  pushMain (pushLetRecs #[] letRecClosures letRecKind letRecMods) sectionVars mainHeaders mainVals
+  -- Store in recFVarIds the fvarId of every function being defined by the mutual block.
+  let mainFVarIds := mainFVars.map Expr.fvarId!
+  let recFVarIds  := (letRecsToLift.toArray.map fun toLift => toLift.fvarId) ++ mainFVarIds
+  -- Compute the set of free variables (excluding `recFVarIds`) for each let-rec.
+  let mctx ← getMCtx
+  let freeVarMap := mkFreeVarMap mctx sectionVars mainFVarIds recFVarIds letRecsToLift
+  resetZetaFVarIds
+  withTrackingZeta do
+    -- By checking `toLift.type` and `toLift.val` we populate `zetaFVarIds`. See comments at `src/Lean/Meta/Closure.lean`.
+    letRecsToLift.forM fun toLift => withLCtx toLift.lctx toLift.localInstances do Meta.check toLift.type; Meta.check toLift.val
+    let letRecClosures ← mkLetRecClosures letRecsToLift freeVarMap
+    -- mkLetRecClosures assign metavariables that were placeholders for the lifted declarations.
+    let mainVals    ← mainVals.mapM instantiateMVars
+    let mainHeaders ← mainHeaders.mapM instantiateMVarsAtHeader
+    let letRecClosures ← letRecClosures.mapM fun closure => do pure { closure with toLift := (← instantiateMVarsAtLetRecToLift closure.toLift) }
+    -- Replace fvarIds for functions being defined with closed terms
+    let r              := insertReplacementForMainFns {} sectionVars mainHeaders mainFVars
+    let r              := insertReplacementForLetRecs r letRecClosures
+    let mainVals       := mainVals.map r.apply
+    let mainHeaders    := mainHeaders.map fun h => { h with type := r.apply h.type }
+    let letRecClosures := letRecClosures.map fun c => { c with toLift := { c.toLift with type := r.apply c.toLift.type, val := r.apply c.toLift.val } }
+    let letRecKind     := getKindForLetRecs mainHeaders
+    let letRecMods     := getModifiersForLetRecs mainHeaders
+    pushMain (pushLetRecs #[] letRecClosures letRecKind letRecMods) sectionVars mainHeaders mainVals
 
 end MutualClosure
 
 private def getAllUserLevelNames (headers : Array DefViewElabHeader) : List Name :=
-if h : 0 < headers.size then
-  -- Recall that all top-level functions must have the same levels. See `check` method above
-  (headers.get ⟨0, h⟩).levelNames
-else
-  []
+  if h : 0 < headers.size then
+    -- Recall that all top-level functions must have the same levels. See `check` method above
+    (headers.get ⟨0, h⟩).levelNames
+  else
+    []
 
 def elabMutualDef (vars : Array Expr) (views : Array DefView) : TermElabM Unit := do
-let scopeLevelNames ← getLevelNames
-let headers ← elabHeaders views
-let allUserLevelNames := getAllUserLevelNames headers
-withFunLocalDecls headers fun funFVars => do
-  let values ← elabFunValues headers
-  Term.synthesizeSyntheticMVarsNoPostponing
-  if isExample views then
-    pure ()
-  else
-    let values ← values.mapM instantiateMVars
-    let headers ← headers.mapM instantiateMVarsAtHeader
-    let letRecsToLift ← getLetRecsToLift
-    let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
-    checkLetRecsToLiftTypes funFVars letRecsToLift
-    withUsedWhen vars headers values letRecsToLift (not $ isTheorem views) fun vars => do
-      let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
-      let preDefs ← levelMVarToParamPreDecls preDefs
-      let preDefs ← instantiateMVarsAtPreDecls preDefs
-      let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
-      addPreDefinitions preDefs
+  let scopeLevelNames ← getLevelNames
+  let headers ← elabHeaders views
+  let allUserLevelNames := getAllUserLevelNames headers
+  withFunLocalDecls headers fun funFVars => do
+    let values ← elabFunValues headers
+    Term.synthesizeSyntheticMVarsNoPostponing
+    if isExample views then
+      pure ()
+    else
+      let values ← values.mapM instantiateMVars
+      let headers ← headers.mapM instantiateMVarsAtHeader
+      let letRecsToLift ← getLetRecsToLift
+      let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
+      checkLetRecsToLiftTypes funFVars letRecsToLift
+      withUsedWhen vars headers values letRecsToLift (not $ isTheorem views) fun vars => do
+        let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
+        let preDefs ← levelMVarToParamPreDecls preDefs
+        let preDefs ← instantiateMVarsAtPreDecls preDefs
+        let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
+        addPreDefinitions preDefs
 
 end Term
 namespace Command
 
 def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
-let views ← ds.mapM fun d => do
-  let modifiers ← elabModifiers d[0]
-  mkDefView modifiers d[1]
-runTermElabM none fun vars => Term.elabMutualDef vars views
+  let views ← ds.mapM fun d => do
+    let modifiers ← elabModifiers d[0]
+    mkDefView modifiers d[1]
+  runTermElabM none fun vars => Term.elabMutualDef vars views
 
 end Command
-end Elab
-end Lean
+end Lean.Elab
diff --git a/stage0/src/Std/Data/RBMap.lean b/stage0/src/Std/Data/RBMap.lean
index 5a40bee28b..d5315d0021 100644
--- a/stage0/src/Std/Data/RBMap.lean
+++ b/stage0/src/Std/Data/RBMap.lean
@@ -8,11 +8,11 @@ namespace Std
 universes u v w w'
 
 inductive Rbcolor
-| red | black
+  | red | black
 
 inductive RBNode (α : Type u) (β : α → Type v)
-| leaf                                                                                        : RBNode α β
-| node  (color : Rbcolor) (lchild : RBNode α β) (key : α) (val : β key) (rchild : RBNode α β) : RBNode α β
+  | leaf                                                                                        : RBNode α β
+  | node  (color : Rbcolor) (lchild : RBNode α β) (key : α) (val : β key) (rchild : RBNode α β) : RBNode α β
 
 namespace RBNode
 variables {α : Type u} {β : α → Type v} {σ : Type w}
@@ -20,188 +20,188 @@ variables {α : Type u} {β : α → Type v} {σ : Type w}
 open Std.Rbcolor Nat
 
 def depth (f : Nat → Nat → Nat) : RBNode α β → Nat
-| leaf           => 0
-| node _ l _ _ r => succ (f (depth f l) (depth f r))
+  | leaf           => 0
+  | node _ l _ _ r => succ (f (depth f l) (depth f r))
 
 protected def min : RBNode α β → Option (Sigma (fun k => β k))
-| leaf              => none
-| node _ leaf k v _ => some ⟨k, v⟩
-| node _ l k v _    => RBNode.min l
+  | leaf              => none
+  | node _ leaf k v _ => some ⟨k, v⟩
+  | node _ l k v _    => RBNode.min l
 
 protected def max : RBNode α β → Option (Sigma (fun k => β k))
-| leaf              => none
-| node _ _ k v leaf => some ⟨k, v⟩
-| node _ _ k v r    => RBNode.max r
+  | leaf              => none
+  | node _ _ k v leaf => some ⟨k, v⟩
+  | node _ _ k v r    => RBNode.max r
 
-@[specialize] def fold (f : σ → ∀ (k : α), β k → σ) : σ → RBNode α β → σ
-| b, leaf           => b
-| b, node _ l k v r => fold f (f (fold f b l) k v) r
+@[specialize] def fold (f : σ → (k : α) → β k → σ) : (init : σ) → RBNode α β → σ
+  | b, leaf           => b
+  | b, node _ l k v r => fold f (f (fold f b l) k v) r
 
-@[specialize] def foldM {m : Type w → Type w'} [Monad m] (f : σ → ∀ (k : α), β k → m σ) (b : σ) : RBNode α β → m σ
-| leaf           => pure b
-| node _ l k v r => do
-  let b ← foldM f b l
-  let b ← f b k v
-  foldM f b r
+@[specialize] def foldM {m : Type w → Type w'} [Monad m] (f : σ → (k : α) → β k → m σ) : (init : σ) → RBNode α β → m σ
+  | b, leaf           => pure b
+  | b, node _ l k v r => do
+    let b ← foldM f b l
+    let b ← f b k v
+    foldM f b r
 
-@[specialize] def revFold (f : σ → ∀ (k : α), β k → σ) (b : σ) : RBNode α β → σ
-| leaf           => b
-| node _ l k v r => revFold f (f (revFold f b r) k v) l
+@[specialize] def revFold (f : σ → (k : α) → β k → σ) : (init : σ) → RBNode α β → σ
+  | b, leaf           => b
+  | b, node _ l k v r => revFold f (f (revFold f b r) k v) l
 
-@[specialize] def all (p : ∀ k, β k → Bool) : RBNode α β → Bool
-| leaf           => true
-| node _ l k v r => p k v && all p l && all p r
+@[specialize] def all (p : (k : α) → β k → Bool) : RBNode α β → Bool
+  | leaf           => true
+  | node _ l k v r => p k v && all p l && all p r
 
-@[specialize] def any (p : ∀ k, β k → Bool) : RBNode α β → Bool
-| leaf             => false
-| node _ l k v r => p k v || any p l || any p r
+@[specialize] def any (p : (k : α) → β k → Bool) : RBNode α β → Bool
+  | leaf             => false
+  | node _ l k v r => p k v || any p l || any p r
 
 def singleton (k : α) (v : β k) : RBNode α β :=
-node red leaf k v leaf
+  node red leaf k v leaf
 
 @[inline] def balance1 : (a : α) → β a → RBNode α β → RBNode α β → RBNode α β
-| kv, vv, t, node _ (node red l kx vx r₁) ky vy r₂   => node red (node black l kx vx r₁) ky vy (node black r₂ kv vv t)
-| kv, vv, t, node _ l₁ ky vy (node red l₂ kx vx r)   => node red (node black l₁ ky vy l₂) kx vx (node black r kv vv t)
-| kv, vv, t, node _ l  ky vy r                       => node black (node red l ky vy r) kv vv t
-| _,  _,  _,                                       _ => leaf -- unreachable
+  | kv, vv, t, node _ (node red l kx vx r₁) ky vy r₂   => node red (node black l kx vx r₁) ky vy (node black r₂ kv vv t)
+  | kv, vv, t, node _ l₁ ky vy (node red l₂ kx vx r)   => node red (node black l₁ ky vy l₂) kx vx (node black r kv vv t)
+  | kv, vv, t, node _ l  ky vy r                       => node black (node red l ky vy r) kv vv t
+  | _,  _,  _,                                       _ => leaf -- unreachable
 
 @[inline] def balance2 : RBNode α β → (a : α) → β a → RBNode α β → RBNode α β
-| t, kv, vv, node _ (node red l kx₁ vx₁ r₁) ky vy r₂  => node red (node black t kv vv l) kx₁ vx₁ (node black r₁ ky vy r₂)
-| t, kv, vv, node _ l₁ ky vy (node red l₂ kx₂ vx₂ r₂) => node red (node black t kv vv l₁) ky vy (node black l₂ kx₂ vx₂ r₂)
-| t, kv, vv, node _ l ky vy r                         => node black t kv vv (node red l ky vy r)
-| _, _,  _,                                        _  => leaf -- unreachable
+  | t, kv, vv, node _ (node red l kx₁ vx₁ r₁) ky vy r₂  => node red (node black t kv vv l) kx₁ vx₁ (node black r₁ ky vy r₂)
+  | t, kv, vv, node _ l₁ ky vy (node red l₂ kx₂ vx₂ r₂) => node red (node black t kv vv l₁) ky vy (node black l₂ kx₂ vx₂ r₂)
+  | t, kv, vv, node _ l ky vy r                         => node black t kv vv (node red l ky vy r)
+  | _, _,  _,                                        _  => leaf -- unreachable
 
 def isRed : RBNode α β → Bool
-| node red _ _ _ _ => true
-| _                => false
+  | node red .. => true
+  | _           => false
 
 def isBlack : RBNode α β → Bool
-| node black _ _ _ _ => true
-| _                  => false
+  | node black .. => true
+  | _             => false
 
 section Insert
 
 variables (lt : α → α → Bool)
 
-@[specialize] def ins : RBNode α β → ∀ k, β k → RBNode α β
-| leaf,               kx, vx => node red leaf kx vx leaf
-| node red a ky vy b, kx, vx =>
-   if lt kx ky then node red (ins a kx vx) ky vy b
-   else if lt ky kx then node red a ky vy (ins b kx vx)
-   else node red a kx vx b
-| node black a ky vy b, kx, vx =>
-    if lt kx ky then
-      if isRed a then balance1 ky vy b (ins a kx vx)
-      else node black (ins a kx vx) ky vy b
-    else if lt ky kx then
-      if isRed b then balance2 a ky vy (ins b kx vx)
-      else node black a ky vy (ins b kx vx)
-    else
-       node black a kx vx b
+@[specialize] def ins : RBNode α β → (k : α) → β k → RBNode α β
+  | leaf,               kx, vx => node red leaf kx vx leaf
+  | node red a ky vy b, kx, vx =>
+     if lt kx ky then node red (ins a kx vx) ky vy b
+     else if lt ky kx then node red a ky vy (ins b kx vx)
+     else node red a kx vx b
+  | node black a ky vy b, kx, vx =>
+      if lt kx ky then
+        if isRed a then balance1 ky vy b (ins a kx vx)
+        else node black (ins a kx vx) ky vy b
+      else if lt ky kx then
+        if isRed b then balance2 a ky vy (ins b kx vx)
+        else node black a ky vy (ins b kx vx)
+      else
+         node black a kx vx b
 
 def setBlack : RBNode α β → RBNode α β
-| node _ l k v r => node black l k v r
-| e              => e
+  | node _ l k v r => node black l k v r
+  | e              => e
 
 @[specialize] def insert (t : RBNode α β) (k : α) (v : β k) : RBNode α β :=
-if isRed t then setBlack (ins lt t k v)
-else ins lt t k v
+  if isRed t then setBlack (ins lt t k v)
+  else ins lt t k v
 
 end Insert
 
 def balance₃ (a : RBNode α β) (k : α) (v : β k) (d : RBNode α β) : RBNode α β :=
-match a with
-| node red (node red a kx vx b) ky vy c => node red (node black a kx vx b) ky vy (node black c k v d)
-| node red a kx vx (node red b ky vy c) => node red (node black a kx vx b) ky vy (node black c k v d)
-| a => match d with
-  | node red b ky vy (node red c kz vz d)   => node red (node black a k v b) ky vy (node black c kz vz d)
-  | node red (node red b ky vy c) kz vz d   => node red (node black a k v b) ky vy (node black c kz vz d)
-  | _                                       => node black a k v d
+  match a with
+  | node red (node red a kx vx b) ky vy c => node red (node black a kx vx b) ky vy (node black c k v d)
+  | node red a kx vx (node red b ky vy c) => node red (node black a kx vx b) ky vy (node black c k v d)
+  | a => match d with
+    | node red b ky vy (node red c kz vz d)   => node red (node black a k v b) ky vy (node black c kz vz d)
+    | node red (node red b ky vy c) kz vz d   => node red (node black a k v b) ky vy (node black c kz vz d)
+    | _                                       => node black a k v d
 
 def setRed : RBNode α β → RBNode α β
-| node _ a k v b => node red a k v b
-| e              => e
+  | node _ a k v b => node red a k v b
+  | e              => e
 
-def balLeft : RBNode α β → ∀ k, β k → RBNode α β → RBNode α β
-| node red a kx vx b,   k, v, r                    => node red (node black a kx vx b) k v r
-| l, k, v, node black a ky vy b                    => balance₃ l k v (node red a ky vy b)
-| l, k, v, node red (node black a ky vy b) kz vz c => node red (node black l k v a) ky vy (balance₃ b kz vz (setRed c))
-| l, k, v, r                                       => node red l k v r -- unreachable
+def balLeft : RBNode α β → (k : α) → β k → RBNode α β → RBNode α β
+  | node red a kx vx b,   k, v, r                    => node red (node black a kx vx b) k v r
+  | l, k, v, node black a ky vy b                    => balance₃ l k v (node red a ky vy b)
+  | l, k, v, node red (node black a ky vy b) kz vz c => node red (node black l k v a) ky vy (balance₃ b kz vz (setRed c))
+  | l, k, v, r                                       => node red l k v r -- unreachable
 
 def balRight (l : RBNode α β) (k : α) (v : β k) (r : RBNode α β) : RBNode α β :=
-match r with
-| (node red b ky vy c) => node red l k v (node black b ky vy c)
-| _ => match l with
-  | node black a kx vx b                    => balance₃ (node red a kx vx b) k v r
-  | node red a kx vx (node black b ky vy c) => node red (balance₃ (setRed a) kx vx b) ky vy (node black c k v r)
-  | _                                       => node red l k v r -- unreachable
+  match r with
+  | (node red b ky vy c) => node red l k v (node black b ky vy c)
+  | _ => match l with
+    | node black a kx vx b                    => balance₃ (node red a kx vx b) k v r
+    | node red a kx vx (node black b ky vy c) => node red (balance₃ (setRed a) kx vx b) ky vy (node black c k v r)
+    | _                                       => node red l k v r -- unreachable
 
 -- TODO: use wellfounded recursion
 partial def appendTrees :  RBNode α β → RBNode α β → RBNode α β
-| leaf, x => x
-| x, leaf => x
-| node red a kx vx b,   node red c ky vy d   =>
-  match appendTrees b c with
-  | node red b' kz vz c' => node red (node red a kx vx b') kz vz (node red c' ky vy d)
-  | bc                   => node red a kx vx (node red bc ky vy d)
-| node black a kx vx b,   node black c ky vy d   =>
-   match appendTrees b c with
-   | node red b' kz vz c' => node red (node black a kx vx b') kz vz (node black c' ky vy d)
-   | bc                   => balLeft a kx vx (node black bc ky vy d)
- | a, node red b kx vx c   => node red (appendTrees a b) kx vx c
- | node red a kx vx b,   c => node red a kx vx (appendTrees b c)
+  | leaf, x => x
+  | x, leaf => x
+  | node red a kx vx b,   node red c ky vy d   =>
+    match appendTrees b c with
+    | node red b' kz vz c' => node red (node red a kx vx b') kz vz (node red c' ky vy d)
+    | bc                   => node red a kx vx (node red bc ky vy d)
+  | node black a kx vx b,   node black c ky vy d   =>
+     match appendTrees b c with
+     | node red b' kz vz c' => node red (node black a kx vx b') kz vz (node black c' ky vy d)
+     | bc                   => balLeft a kx vx (node black bc ky vy d)
+   | a, node red b kx vx c   => node red (appendTrees a b) kx vx c
+   | node red a kx vx b,   c => node red a kx vx (appendTrees b c)
 
 section Erase
 
 variables (lt : α → α → Bool)
 
 @[specialize] def del (x : α) : RBNode α β → RBNode α β
-| leaf           => leaf
-| node _ a y v b =>
-  if lt x y then
-    if a.isBlack then balLeft (del x a) y v b
-    else node red (del x a) y v b
-  else if lt y x then
-    if b.isBlack then balRight a y v (del x b)
-    else node red a y v (del x b)
-  else appendTrees a b
+  | leaf           => leaf
+  | node _ a y v b =>
+    if lt x y then
+      if a.isBlack then balLeft (del x a) y v b
+      else node red (del x a) y v b
+    else if lt y x then
+      if b.isBlack then balRight a y v (del x b)
+      else node red a y v (del x b)
+    else appendTrees a b
 
 @[specialize] def erase (x : α) (t : RBNode α β) : RBNode α β :=
-let t := del lt x t;
-t.setBlack
+  let t := del lt x t;
+  t.setBlack
 
 end Erase
 
 section Membership
 variable (lt : α → α → Bool)
 
-@[specialize] def findCore : RBNode α β → ∀ (k : α), Option (Sigma (fun k => β k))
-| leaf,             x => none
-| node _ a ky vy b, x =>
-   if lt x ky then findCore a x
-   else if lt ky x then findCore b x
-   else some ⟨ky, vy⟩
+@[specialize] def findCore : RBNode α β → (k : α) → Option (Sigma (fun k => β k))
+  | leaf,             x => none
+  | node _ a ky vy b, x =>
+     if lt x ky then findCore a x
+     else if lt ky x then findCore b x
+     else some ⟨ky, vy⟩
 
 @[specialize] def find {β : Type v} : RBNode α (fun _ => β) → α → Option β
-| leaf,             x => none
-| node _ a ky vy b, x =>
-  if lt x ky then find a x
-  else if lt ky x then find b x
-  else some vy
+  | leaf,             x => none
+  | node _ a ky vy b, x =>
+    if lt x ky then find a x
+    else if lt ky x then find b x
+    else some vy
 
 @[specialize] def lowerBound : RBNode α β → α → Option (Sigma β) → Option (Sigma β)
-| leaf,             x, lb => lb
-| node _ a ky vy b, x, lb =>
-  if lt x ky then lowerBound a x lb
-  else if lt ky x then lowerBound b x (some ⟨ky, vy⟩)
-  else some ⟨ky, vy⟩
+  | leaf,             x, lb => lb
+  | node _ a ky vy b, x, lb =>
+    if lt x ky then lowerBound a x lb
+    else if lt ky x then lowerBound b x (some ⟨ky, vy⟩)
+    else some ⟨ky, vy⟩
 
 end Membership
 
 inductive WellFormed (lt : α → α → Bool) : RBNode α β → Prop
-| leafWff : WellFormed lt leaf
-| insertWff {n n' : RBNode α β} {k : α} {v : β k} : WellFormed lt n → n' = insert lt n k v → WellFormed lt n'
-| eraseWff {n n' : RBNode α β} {k : α} : WellFormed lt n → n' = erase lt k n → WellFormed lt n'
+  | leafWff : WellFormed lt leaf
+  | insertWff {n n' : RBNode α β} {k : α} {v : β k} : WellFormed lt n → n' = insert lt n k v → WellFormed lt n'
+  | eraseWff {n n' : RBNode α β} {k : α} : WellFormed lt n → n' = erase lt k n → WellFormed lt n'
 
 end RBNode
 
@@ -210,117 +210,117 @@ open Std.RBNode
 /- TODO(Leo): define dRBMap -/
 
 def RBMap (α : Type u) (β : Type v) (lt : α → α → Bool) : Type (max u v) :=
-{t : RBNode α (fun _ => β) // t.WellFormed lt }
+  {t : RBNode α (fun _ => β) // t.WellFormed lt }
 
 @[inline] def mkRBMap (α : Type u) (β : Type v) (lt : α → α → Bool) : RBMap α β lt :=
-⟨leaf, WellFormed.leafWff⟩
+  ⟨leaf, WellFormed.leafWff⟩
 
 @[inline] def RBMap.empty {α : Type u} {β : Type v} {lt : α → α → Bool} : RBMap α β lt :=
-mkRBMap _ _ _
+  mkRBMap ..
 
 instance (α : Type u) (β : Type v) (lt : α → α → Bool) : HasEmptyc (RBMap α β lt) :=
-⟨RBMap.empty⟩
+  ⟨RBMap.empty⟩
 
 namespace RBMap
 variables {α : Type u} {β : Type v} {σ : Type w} {lt : α → α → Bool}
 
 def depth (f : Nat → Nat → Nat) (t : RBMap α β lt) : Nat :=
-t.val.depth f
+  t.val.depth f
 
-@[inline] def fold (f : σ → α → β → σ) : σ → RBMap α β lt → σ
-| b, ⟨t, _⟩ => t.fold f b
+@[inline] def fold (f : σ → α → β → σ) : (init : σ) → RBMap α β lt → σ
+  | b, ⟨t, _⟩ => t.fold f b
 
-@[inline] def revFold (f : σ → α → β → σ) : σ → RBMap α β lt → σ
-| b, ⟨t, _⟩ => t.revFold f b
+@[inline] def revFold (f : σ → α → β → σ) : (init : σ) → RBMap α β lt → σ
+  | b, ⟨t, _⟩ => t.revFold f b
 
-@[inline] def foldM {m : Type w → Type w'} [Monad m] (f : σ → α → β → m σ) : σ → RBMap α β lt → m σ
-| b, ⟨t, _⟩ => t.foldM f b
+@[inline] def foldM {m : Type w → Type w'} [Monad m] (f : σ → α → β → m σ) : (init : σ) → RBMap α β lt → m σ
+  | b, ⟨t, _⟩ => t.foldM f b
 
 @[inline] def forM {m : Type w → Type w'} [Monad m] (f : α → β → m PUnit) (t : RBMap α β lt) : m PUnit :=
-t.foldM (fun _ k v => f k v) ⟨⟩
+  t.foldM (fun _ k v => f k v) ⟨⟩
 
 @[inline] def isEmpty : RBMap α β lt → Bool
-| ⟨leaf, _⟩ => true
-| _         => false
+  | ⟨leaf, _⟩ => true
+  | _         => false
 
 @[specialize] def toList : RBMap α β lt → List (α × β)
-| ⟨t, _⟩ => t.revFold (fun ps k v => (k, v)::ps) []
+  | ⟨t, _⟩ => t.revFold (fun ps k v => (k, v)::ps) []
 
 @[inline] protected def min : RBMap α β lt → Option (α × β)
-| ⟨t, _⟩ =>
-  match t.min with
-  | some ⟨k, v⟩ => some (k, v)
-  | none        => none
+  | ⟨t, _⟩ =>
+    match t.min with
+    | some ⟨k, v⟩ => some (k, v)
+    | none        => none
 
 @[inline] protected def max : RBMap α β lt → Option (α × β)
-| ⟨t, _⟩ =>
-  match t.max with
-  | some ⟨k, v⟩ => some (k, v)
-  | none        => none
+  | ⟨t, _⟩ =>
+    match t.max with
+    | some ⟨k, v⟩ => some (k, v)
+    | none        => none
 
 instance [HasRepr α] [HasRepr β] : HasRepr (RBMap α β lt) :=
-⟨fun t => "rbmapOf " ++ repr t.toList⟩
+  ⟨fun t => "rbmapOf " ++ repr t.toList⟩
 
 @[inline] def insert : RBMap α β lt → α → β → RBMap α β lt
-| ⟨t, w⟩, k, v => ⟨t.insert lt k v, WellFormed.insertWff w rfl⟩
+  | ⟨t, w⟩, k, v => ⟨t.insert lt k v, WellFormed.insertWff w rfl⟩
 
 @[inline] def erase : RBMap α β lt → α → RBMap α β lt
-| ⟨t, w⟩, k => ⟨t.erase lt k, WellFormed.eraseWff w rfl⟩
+  | ⟨t, w⟩, k => ⟨t.erase lt k, WellFormed.eraseWff w rfl⟩
 
 @[specialize] def ofList : List (α × β) → RBMap α β lt
-| []        => mkRBMap _ _ _
-| ⟨k,v⟩::xs => (ofList xs).insert k v
+  | []        => mkRBMap ..
+  | ⟨k,v⟩::xs => (ofList xs).insert k v
 
 @[inline] def findCore? : RBMap α β lt → α → Option (Sigma (fun (k : α) => β))
-| ⟨t, _⟩, x => t.findCore lt x
+  | ⟨t, _⟩, x => t.findCore lt x
 
 @[inline] def find? : RBMap α β lt → α → Option β
-| ⟨t, _⟩, x => t.find lt x
+  | ⟨t, _⟩, x => t.find lt x
 
 @[inline] def findD (t : RBMap α β lt) (k : α) (v₀ : β) : β :=
-(t.find? k).getD v₀
+  (t.find? k).getD v₀
 
 /-- (lowerBound k) retrieves the kv pair of the largest key smaller than or equal to `k`,
     if it exists. -/
 @[inline] def lowerBound : RBMap α β lt → α → Option (Sigma (fun (k : α) => β))
-| ⟨t, _⟩, x => t.lowerBound lt x none
+  | ⟨t, _⟩, x => t.lowerBound lt x none
 
 @[inline] def contains (t : RBMap α β lt) (a : α) : Bool :=
-(t.find? a).isSome
+  (t.find? a).isSome
 
 @[inline] def fromList (l : List (α × β)) (lt : α → α → Bool) : RBMap α β lt :=
-l.foldl (fun r p => r.insert p.1 p.2) (mkRBMap α β lt)
+  l.foldl (fun r p => r.insert p.1 p.2) (mkRBMap α β lt)
 
 @[inline] def all : RBMap α β lt → (α → β → Bool) → Bool
-| ⟨t, _⟩, p => t.all p
+  | ⟨t, _⟩, p => t.all p
 
 @[inline] def any : RBMap α β lt → (α → β → Bool) → Bool
-| ⟨t, _⟩, p => t.any p
+  | ⟨t, _⟩, p => t.any p
 
 def size (m : RBMap α β lt) : Nat :=
-m.fold (fun sz _ _ => sz+1) 0
+  m.fold (fun sz _ _ => sz+1) 0
 
 def maxDepth (t : RBMap α β lt) : Nat :=
-t.val.depth Nat.max
+  t.val.depth Nat.max
 
 @[inline] def min! [Inhabited α] [Inhabited β] (t : RBMap α β lt) : α × β :=
-match t.min with
-| some p => p
-| none   => panic! "map is empty"
+  match t.min with
+  | some p => p
+  | none   => panic! "map is empty"
 
 @[inline] def max! [Inhabited α] [Inhabited β] (t : RBMap α β lt) : α × β :=
-match t.max with
-| some p => p
-| none   => panic! "map is empty"
+  match t.max with
+  | some p => p
+  | none   => panic! "map is empty"
 
 @[inline] def find! [Inhabited β] (t : RBMap α β lt) (k : α) : β :=
-match t.find? k with
-| some b => b
-| none   => panic! "key is not in the map"
+  match t.find? k with
+  | some b => b
+  | none   => panic! "key is not in the map"
 
 end RBMap
 
 def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (lt : α → α → Bool) : RBMap α β lt :=
-RBMap.fromList l lt
+  RBMap.fromList l lt
 
 end Std
diff --git a/stage0/src/Std/Data/RBTree.lean b/stage0/src/Std/Data/RBTree.lean
index 424e9ed057..538afe0dae 100644
--- a/stage0/src/Std/Data/RBTree.lean
+++ b/stage0/src/Std/Data/RBTree.lean
@@ -9,89 +9,89 @@ namespace Std
 universes u v w
 
 def RBTree (α : Type u) (lt : α → α → Bool) : Type u :=
-RBMap α Unit lt
+  RBMap α Unit lt
 
 @[inline] def mkRBTree (α : Type u) (lt : α → α → Bool) : RBTree α lt :=
-mkRBMap α Unit lt
+  mkRBMap α Unit lt
 
-instance RBTree.hasEmptyc (α : Type u) (lt : α → α → Bool) : HasEmptyc (RBTree α lt) :=
-⟨mkRBTree α lt⟩
+instance (α : Type u) (lt : α → α → Bool) : HasEmptyc (RBTree α lt) :=
+  ⟨mkRBTree α lt⟩
 
 namespace RBTree
 variables {α : Type u} {β : Type v} {lt : α → α → Bool}
 
 @[inline] def empty : RBTree α lt :=
-RBMap.empty
+  RBMap.empty
 
 @[inline] def depth (f : Nat → Nat → Nat) (t : RBTree α lt) : Nat :=
-RBMap.depth f t
+  RBMap.depth f t
 
-@[inline] def fold (f : β → α → β) (b : β) (t : RBTree α lt) : β :=
-RBMap.fold (fun r a _ => f r a) b t
+@[inline] def fold (f : β → α → β) (init : β) (t : RBTree α lt) : β :=
+  RBMap.fold (fun r a _ => f r a) init t
 
-@[inline] def revFold (f : β → α → β) (b : β) (t : RBTree α lt) : β :=
-RBMap.revFold (fun r a _ => f r a) b t
+@[inline] def revFold (f : β → α → β) (init : β) (t : RBTree α lt) : β :=
+  RBMap.revFold (fun r a _ => f r a) init t
 
-@[inline] def foldM {m : Type v → Type w} [Monad m] (f : β → α → m β) (b : β) (t : RBTree α lt) : m β :=
-RBMap.foldM (fun r a _ => f r a) b t
+@[inline] def foldM {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (t : RBTree α lt) : m β :=
+  RBMap.foldM (fun r a _ => f r a) init t
 
 @[inline] def forM {m : Type v → Type w} [Monad m] (f : α → m PUnit) (t : RBTree α lt) : m PUnit :=
-t.foldM (fun _ a => f a) ⟨⟩
+  t.foldM (fun _ a => f a) ⟨⟩
 
 @[inline] def isEmpty (t : RBTree α lt) : Bool :=
-RBMap.isEmpty t
+  RBMap.isEmpty t
 
 @[specialize] def toList (t : RBTree α lt) : List α :=
-t.revFold (fun as a => a::as) []
+  t.revFold (fun as a => a::as) []
 
 @[inline] protected def min (t : RBTree α lt) : Option α :=
-match RBMap.min t with
-| some ⟨a, _⟩ => some a
-| none        => none
+  match RBMap.min t with
+  | some ⟨a, _⟩ => some a
+  | none        => none
 
 @[inline] protected def max (t : RBTree α lt) : Option α :=
-match RBMap.max t with
-| some ⟨a, _⟩ => some a
-| none        => none
+  match RBMap.max t with
+  | some ⟨a, _⟩ => some a
+  | none        => none
 
 instance [HasRepr α] : HasRepr (RBTree α lt) :=
-⟨fun t => "rbtreeOf " ++ repr t.toList⟩
+  ⟨fun t => "rbtreeOf " ++ repr t.toList⟩
 
 @[inline] def insert (t : RBTree α lt) (a : α) : RBTree α lt :=
-RBMap.insert t a ()
+  RBMap.insert t a ()
 
 @[inline] def erase (t : RBTree α lt) (a : α) : RBTree α lt :=
-RBMap.erase t a
+  RBMap.erase t a
 
 @[specialize] def ofList : List α → RBTree α lt
-| []    => mkRBTree _ _
-| x::xs => (ofList xs).insert x
+  | []    => mkRBTree ..
+  | x::xs => (ofList xs).insert x
 
 @[inline] def find? (t : RBTree α lt) (a : α) : Option α :=
-match RBMap.findCore? t a with
-| some ⟨a, _⟩ => some a
-| none        => none
+  match RBMap.findCore? t a with
+  | some ⟨a, _⟩ => some a
+  | none        => none
 
 @[inline] def contains (t : RBTree α lt) (a : α) : Bool :=
-(t.find? a).isSome
+  (t.find? a).isSome
 
 def fromList (l : List α) (lt : α → α → Bool) : RBTree α lt :=
-l.foldl insert (mkRBTree α lt)
+  l.foldl insert (mkRBTree α lt)
 
 @[inline] def all (t : RBTree α lt) (p : α → Bool) : Bool :=
-RBMap.all t (fun a _ => p a)
+  RBMap.all t (fun a _ => p a)
 
 @[inline] def any (t : RBTree α lt) (p : α → Bool) : Bool :=
-RBMap.any t (fun a _ => p a)
+  RBMap.any t (fun a _ => p a)
 
 def subset (t₁ t₂ : RBTree α lt) : Bool :=
-t₁.all $ fun a => (t₂.find? a).toBool
+  t₁.all fun a => (t₂.find? a).toBool
 
 def seteq (t₁ t₂ : RBTree α lt) : Bool :=
-subset t₁ t₂ && subset t₂ t₁
+  subset t₁ t₂ && subset t₂ t₁
 
 end RBTree
 
 def rbtreeOf {α : Type u} (l : List α) (lt : α → α → Bool) : RBTree α lt :=
-RBTree.fromList l lt
+  RBTree.fromList l lt
 end Std
diff --git a/stage0/stdlib/Lean/Elab/MutualDef.c b/stage0/stdlib/Lean/Elab/MutualDef.c
index 223fabd707..4ee968ca68 100644
--- a/stage0/stdlib/Lean/Elab/MutualDef.c
+++ b/stage0/stdlib/Lean/Elab/MutualDef.c
@@ -60,7 +60,6 @@ lean_object* l_Lean_Elab_Term_MutualClosure_ClosureState_exprArgs___default;
 lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_check___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkClosureForAux___closed__4;
 lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_check___lambda__6___closed__3;
-lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkClosureForAux_match__3___rarg(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_FixPoint_markModified___rarg(lean_object*);
 lean_object* l_Lean_CollectFVars_main(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabMutualDef___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -147,7 +146,6 @@ lean_object* l_Lean_Elab_Term_withLevelNames___rarg(lean_object*, lean_object*,
 lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_collectUsed___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_umapMAux___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkClosureForAux___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_check___lambda__7___closed__1;
-lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkClosureForAux_match__3(lean_object*);
 lean_object* l_List_foldl___main___at_Lean_Elab_Term_MutualClosure_pushLetRecs___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_LocalContext_contains(lean_object*, lean_object*);
 uint8_t l_Lean_Elab_DefKind_isExample(uint8_t);
@@ -8298,22 +8296,6 @@ x_2 = lean_alloc_closure((void*)(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Te
 return x_2;
 }
 }
-lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkClosureForAux_match__3___rarg(lean_object* x_1, lean_object* x_2) {
-_start:
-{
-lean_object* x_3; 
-x_3 = lean_apply_1(x_2, x_1);
-return x_3;
-}
-}
-lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkClosureForAux_match__3(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkClosureForAux_match__3___rarg), 2, 0);
-return x_2;
-}
-}
 lean_object* l_Array_erase___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkClosureForAux___spec__1(lean_object* x_1, lean_object* x_2) {
 _start:
 {
diff --git a/stage0/stdlib/Std/Data/RBMap.c b/stage0/stdlib/Std/Data/RBMap.c
index 4c564c89e8..55eaed1b4f 100644
--- a/stage0/stdlib/Std/Data/RBMap.c
+++ b/stage0/stdlib/Std/Data/RBMap.c
@@ -115,7 +115,7 @@ lean_object* l_Std_RBNode_balance_u2083_match__2___rarg(lean_object*, lean_objec
 lean_object* l_Std_RBNode_min_match__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBMap_insert_match__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_rbmapOf___rarg(lean_object*, lean_object*);
-lean_object* l_Std_RBNode_foldM_match__1___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Std_RBNode_foldM_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBMap_any(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBMap_min_x21_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBMap_find_x3f(lean_object*, lean_object*);
@@ -174,7 +174,7 @@ lean_object* l_Std_RBMap_max___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBMap_max_match__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_appendTrees_match__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBMap_max_x21___rarg(lean_object*, lean_object*, lean_object*);
-lean_object* l_Std_RBNode_revFold_match__1(lean_object*, lean_object*, lean_object*);
+lean_object* l_Std_RBNode_revFold_match__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_findCore_match__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_ins_match__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_balance1(lean_object*, lean_object*);
@@ -193,7 +193,7 @@ lean_object* l_Std_RBMap_max_x21(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBMap_isEmpty_match__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_balance1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_appendTrees_match__2(lean_object*, lean_object*, lean_object*);
-lean_object* l_Std_RBNode_foldM_match__1(lean_object*, lean_object*, lean_object*);
+lean_object* l_Std_RBNode_foldM_match__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_isRed_match__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_ins(lean_object*, lean_object*);
 lean_object* l_Std_RBNode_max_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -245,7 +245,7 @@ lean_object* l_Std_RBMap_forM___boxed(lean_object*, lean_object*, lean_object*,
 lean_object* l_Std_RBMap_forM___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBMap_min_x21(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBMap_maxDepth___rarg___closed__1;
-lean_object* l_Std_RBNode_revFold_match__1___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Std_RBNode_revFold_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_revFold(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_foldM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_findCore___rarg(lean_object*, lean_object*, lean_object*);
@@ -697,43 +697,42 @@ x_4 = lean_alloc_closure((void*)(l_Std_RBNode_fold___rarg), 3, 0);
 return x_4;
 }
 }
-lean_object* l_Std_RBNode_foldM_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_Std_RBNode_foldM_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
-if (lean_obj_tag(x_1) == 0)
+if (lean_obj_tag(x_2) == 0)
 {
-lean_object* x_4; lean_object* x_5; 
-lean_dec(x_3);
-x_4 = lean_box(0);
-x_5 = lean_apply_1(x_2, x_4);
+lean_object* x_5; 
+lean_dec(x_4);
+x_5 = lean_apply_1(x_3, x_1);
 return x_5;
 }
 else
 {
 uint8_t x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
-lean_dec(x_2);
-x_6 = lean_ctor_get_uint8(x_1, sizeof(void*)*4);
-x_7 = lean_ctor_get(x_1, 0);
+lean_dec(x_3);
+x_6 = lean_ctor_get_uint8(x_2, sizeof(void*)*4);
+x_7 = lean_ctor_get(x_2, 0);
 lean_inc(x_7);
-x_8 = lean_ctor_get(x_1, 1);
+x_8 = lean_ctor_get(x_2, 1);
 lean_inc(x_8);
-x_9 = lean_ctor_get(x_1, 2);
+x_9 = lean_ctor_get(x_2, 2);
 lean_inc(x_9);
-x_10 = lean_ctor_get(x_1, 3);
+x_10 = lean_ctor_get(x_2, 3);
 lean_inc(x_10);
-lean_dec(x_1);
+lean_dec(x_2);
 x_11 = lean_box(x_6);
-x_12 = lean_apply_5(x_3, x_11, x_7, x_8, x_9, x_10);
+x_12 = lean_apply_6(x_4, x_1, x_11, x_7, x_8, x_9, x_10);
 return x_12;
 }
 }
 }
-lean_object* l_Std_RBNode_foldM_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_Std_RBNode_foldM_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
-lean_object* x_4; 
-x_4 = lean_alloc_closure((void*)(l_Std_RBNode_foldM_match__1___rarg), 3, 0);
-return x_4;
+lean_object* x_5; 
+x_5 = lean_alloc_closure((void*)(l_Std_RBNode_foldM_match__1___rarg), 4, 0);
+return x_5;
 }
 }
 lean_object* l_Std_RBNode_foldM___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
@@ -812,43 +811,42 @@ x_5 = lean_alloc_closure((void*)(l_Std_RBNode_foldM___rarg), 4, 0);
 return x_5;
 }
 }
-lean_object* l_Std_RBNode_revFold_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_Std_RBNode_revFold_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
-if (lean_obj_tag(x_1) == 0)
+if (lean_obj_tag(x_2) == 0)
 {
-lean_object* x_4; lean_object* x_5; 
-lean_dec(x_3);
-x_4 = lean_box(0);
-x_5 = lean_apply_1(x_2, x_4);
+lean_object* x_5; 
+lean_dec(x_4);
+x_5 = lean_apply_1(x_3, x_1);
 return x_5;
 }
 else
 {
 uint8_t x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
-lean_dec(x_2);
-x_6 = lean_ctor_get_uint8(x_1, sizeof(void*)*4);
-x_7 = lean_ctor_get(x_1, 0);
+lean_dec(x_3);
+x_6 = lean_ctor_get_uint8(x_2, sizeof(void*)*4);
+x_7 = lean_ctor_get(x_2, 0);
 lean_inc(x_7);
-x_8 = lean_ctor_get(x_1, 1);
+x_8 = lean_ctor_get(x_2, 1);
 lean_inc(x_8);
-x_9 = lean_ctor_get(x_1, 2);
+x_9 = lean_ctor_get(x_2, 2);
 lean_inc(x_9);
-x_10 = lean_ctor_get(x_1, 3);
+x_10 = lean_ctor_get(x_2, 3);
 lean_inc(x_10);
-lean_dec(x_1);
+lean_dec(x_2);
 x_11 = lean_box(x_6);
-x_12 = lean_apply_5(x_3, x_11, x_7, x_8, x_9, x_10);
+x_12 = lean_apply_6(x_4, x_1, x_11, x_7, x_8, x_9, x_10);
 return x_12;
 }
 }
 }
-lean_object* l_Std_RBNode_revFold_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_Std_RBNode_revFold_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
-lean_object* x_4; 
-x_4 = lean_alloc_closure((void*)(l_Std_RBNode_revFold_match__1___rarg), 3, 0);
-return x_4;
+lean_object* x_5; 
+x_5 = lean_alloc_closure((void*)(l_Std_RBNode_revFold_match__1___rarg), 4, 0);
+return x_5;
 }
 }
 lean_object* l_Std_RBNode_revFold___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
@@ -21600,7 +21598,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
 x_1 = l_Std_RBMap_min_x21___rarg___closed__1;
 x_2 = l_Std_RBMap_min_x21___rarg___closed__2;
 x_3 = lean_unsigned_to_nat(309u);
-x_4 = lean_unsigned_to_nat(12u);
+x_4 = lean_unsigned_to_nat(14u);
 x_5 = l_Std_RBMap_min_x21___rarg___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
 return x_6;
@@ -21713,7 +21711,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
 x_1 = l_Std_RBMap_min_x21___rarg___closed__1;
 x_2 = l_Std_RBMap_max_x21___rarg___closed__1;
 x_3 = lean_unsigned_to_nat(314u);
-x_4 = lean_unsigned_to_nat(12u);
+x_4 = lean_unsigned_to_nat(14u);
 x_5 = l_Std_RBMap_min_x21___rarg___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
 return x_6;
@@ -21834,7 +21832,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
 x_1 = l_Std_RBMap_min_x21___rarg___closed__1;
 x_2 = l_Std_RBMap_find_x21___rarg___closed__1;
 x_3 = lean_unsigned_to_nat(319u);
-x_4 = lean_unsigned_to_nat(12u);
+x_4 = lean_unsigned_to_nat(14u);
 x_5 = l_Std_RBMap_find_x21___rarg___closed__2;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
 return x_6;
diff --git a/stage0/stdlib/Std/Data/RBTree.c b/stage0/stdlib/Std/Data/RBTree.c
index 728c77d79e..6215de9055 100644
--- a/stage0/stdlib/Std/Data/RBTree.c
+++ b/stage0/stdlib/Std/Data/RBTree.c
@@ -18,33 +18,35 @@ lean_object* l_List_repr___rarg(lean_object*, lean_object*);
 lean_object* l_Std_RBTree_ofList_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBTree_toList___rarg___closed__1;
 lean_object* l_Std_RBTree_all___boxed(lean_object*, lean_object*);
+lean_object* l_Std_RBTree_Std_Data_RBTree___instance__2(lean_object*, lean_object*);
 lean_object* l_Std_RBNode_foldM___at_Std_RBTree_foldM___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBTree_toList___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
 uint8_t l_Std_RBNode_any___at_Std_RBTree_any___spec__1___rarg(lean_object*, lean_object*);
 lean_object* l_Std_RBNode_max___rarg(lean_object*);
 lean_object* l_Std_RBTree_forM(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_foldM___at_Std_RBTree_forM___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Std_RBTree_Std_Data_RBTree___instance__2___rarg___closed__1;
 lean_object* l_Std_RBTree_find_x3f___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_mkRBTree(lean_object*, lean_object*);
 lean_object* l_Std_RBTree_subset___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_all___at_Std_RBTree_subset___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_all___at_Std_RBTree_all___spec__1(lean_object*);
 lean_object* l_Std_RBTree_min___rarg(lean_object*);
-lean_object* l_Std_RBTree_hasEmptyc(lean_object*, lean_object*);
 lean_object* lean_string_append(lean_object*, lean_object*);
 lean_object* l_Std_RBNode_foldM___at_Std_RBTree_forM___spec__1___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_foldM___at_Std_RBTree_forM___spec__1(lean_object*, lean_object*);
+lean_object* l_Std_RBTree_Std_Data_RBTree___instance__2___rarg(lean_object*, lean_object*);
 lean_object* l_Std_RBTree_max(lean_object*, lean_object*);
 lean_object* l_Std_RBNode_insert___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBTree_seteq___rarg___boxed(lean_object*, lean_object*, lean_object*);
-lean_object* l_Std_RBTree_Std_Data_RBTree___instance__1___boxed(lean_object*, lean_object*);
 lean_object* l_Std_RBTree_find_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Std_Std_Data_RBTree___instance__1___boxed(lean_object*, lean_object*);
 lean_object* l_Std_RBTree_forM___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBTree_toList___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBTree_seteq(lean_object*);
 lean_object* l_Std_RBNode_all___at_Std_RBTree_all___spec__1___rarg___boxed(lean_object*, lean_object*);
+lean_object* l_Std_RBTree_Std_Data_RBTree___instance__2___boxed(lean_object*, lean_object*);
 lean_object* l_Std_RBTree_depth___rarg___boxed(lean_object*, lean_object*);
-lean_object* l_Std_RBTree_Std_Data_RBTree___instance__1___rarg___closed__1;
 lean_object* l_Std_RBNode_revFold___rarg(lean_object*, lean_object*, lean_object*);
 uint8_t l_Std_RBNode_all___at_Std_RBTree_subset___spec__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBTree_foldM(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -66,7 +68,6 @@ lean_object* l_Std_RBTree_all(lean_object*, lean_object*);
 lean_object* l_Std_RBTree_revFold___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_rbtreeOf___rarg(lean_object*, lean_object*);
 lean_object* l_Std_RBTree_ofList(lean_object*);
-lean_object* l_Std_RBTree_hasEmptyc___boxed(lean_object*, lean_object*);
 lean_object* l_Std_RBNode_min___rarg(lean_object*);
 lean_object* l_Std_RBNode_erase___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_foldM___at_Std_RBTree_forM___spec__1___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -76,6 +77,7 @@ lean_object* l_Std_RBTree_depth___boxed(lean_object*, lean_object*);
 lean_object* l_Std_RBTree_min___boxed(lean_object*, lean_object*);
 lean_object* l_Std_RBTree_empty___boxed(lean_object*, lean_object*);
 lean_object* l_Std_rbtreeOf(lean_object*);
+lean_object* l_Std_Std_Data_RBTree___instance__1(lean_object*, lean_object*);
 lean_object* l_Std_mkRBTree___boxed(lean_object*, lean_object*);
 lean_object* l_Std_RBNode_fold___at_Std_RBTree_fold___spec__1(lean_object*, lean_object*);
 lean_object* l_Std_RBTree_max___rarg___boxed(lean_object*);
@@ -88,7 +90,6 @@ lean_object* l_Std_RBTree_toList(lean_object*, lean_object*);
 lean_object* l_Std_RBTree_empty(lean_object*, lean_object*);
 lean_object* l_Std_RBTree_insert___rarg(lean_object*, lean_object*, lean_object*);
 uint8_t l_Std_RBTree_all___rarg(lean_object*, lean_object*);
-lean_object* l_Std_RBTree_Std_Data_RBTree___instance__1___rarg(lean_object*, lean_object*);
 lean_object* l_Std_RBTree_depth___rarg(lean_object*, lean_object*);
 lean_object* l_Std_RBTree_any___boxed(lean_object*, lean_object*);
 lean_object* l_Std_RBTree_min___rarg___boxed(lean_object*);
@@ -110,7 +111,6 @@ lean_object* l_Std_RBNode_fold___at_Std_RBTree_fold___spec__1___rarg(lean_object
 lean_object* l_List_foldl___main___at_Std_RBTree_fromList___spec__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBTree_erase___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBTree_min(lean_object*, lean_object*);
-lean_object* l_Std_RBTree_Std_Data_RBTree___instance__1(lean_object*, lean_object*);
 lean_object* l_Std_RBTree_fold___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_any___at_Std_RBTree_any___spec__1___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_Std_RBNode_foldM___at_Std_RBTree_foldM___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -144,7 +144,7 @@ lean_dec(x_2);
 return x_3;
 }
 }
-lean_object* l_Std_RBTree_hasEmptyc(lean_object* x_1, lean_object* x_2) {
+lean_object* l_Std_Std_Data_RBTree___instance__1(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
@@ -152,11 +152,11 @@ x_3 = lean_box(0);
 return x_3;
 }
 }
-lean_object* l_Std_RBTree_hasEmptyc___boxed(lean_object* x_1, lean_object* x_2) {
+lean_object* l_Std_Std_Data_RBTree___instance__1___boxed(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
-x_3 = l_Std_RBTree_hasEmptyc(x_1, x_2);
+x_3 = l_Std_Std_Data_RBTree___instance__1(x_1, x_2);
 lean_dec(x_2);
 return x_3;
 }
@@ -844,7 +844,7 @@ lean_dec(x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Std_RBTree_Std_Data_RBTree___instance__1___rarg___closed__1() {
+static lean_object* _init_l_Std_RBTree_Std_Data_RBTree___instance__2___rarg___closed__1() {
 _start:
 {
 lean_object* x_1; 
@@ -852,31 +852,31 @@ x_1 = lean_mk_string("rbtreeOf ");
 return x_1;
 }
 }
-lean_object* l_Std_RBTree_Std_Data_RBTree___instance__1___rarg(lean_object* x_1, lean_object* x_2) {
+lean_object* l_Std_RBTree_Std_Data_RBTree___instance__2___rarg(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_3 = l_Std_RBTree_toList___rarg(x_2);
 x_4 = l_List_repr___rarg(x_1, x_3);
-x_5 = l_Std_RBTree_Std_Data_RBTree___instance__1___rarg___closed__1;
+x_5 = l_Std_RBTree_Std_Data_RBTree___instance__2___rarg___closed__1;
 x_6 = lean_string_append(x_5, x_4);
 lean_dec(x_4);
 return x_6;
 }
 }
-lean_object* l_Std_RBTree_Std_Data_RBTree___instance__1(lean_object* x_1, lean_object* x_2) {
+lean_object* l_Std_RBTree_Std_Data_RBTree___instance__2(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
-x_3 = lean_alloc_closure((void*)(l_Std_RBTree_Std_Data_RBTree___instance__1___rarg), 2, 0);
+x_3 = lean_alloc_closure((void*)(l_Std_RBTree_Std_Data_RBTree___instance__2___rarg), 2, 0);
 return x_3;
 }
 }
-lean_object* l_Std_RBTree_Std_Data_RBTree___instance__1___boxed(lean_object* x_1, lean_object* x_2) {
+lean_object* l_Std_RBTree_Std_Data_RBTree___instance__2___boxed(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 lean_object* x_3; 
-x_3 = l_Std_RBTree_Std_Data_RBTree___instance__1(x_1, x_2);
+x_3 = l_Std_RBTree_Std_Data_RBTree___instance__2(x_1, x_2);
 lean_dec(x_2);
 return x_3;
 }
@@ -1539,8 +1539,8 @@ if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 l_Std_RBTree_toList___rarg___closed__1 = _init_l_Std_RBTree_toList___rarg___closed__1();
 lean_mark_persistent(l_Std_RBTree_toList___rarg___closed__1);
-l_Std_RBTree_Std_Data_RBTree___instance__1___rarg___closed__1 = _init_l_Std_RBTree_Std_Data_RBTree___instance__1___rarg___closed__1();
-lean_mark_persistent(l_Std_RBTree_Std_Data_RBTree___instance__1___rarg___closed__1);
+l_Std_RBTree_Std_Data_RBTree___instance__2___rarg___closed__1 = _init_l_Std_RBTree_Std_Data_RBTree___instance__2___rarg___closed__1();
+lean_mark_persistent(l_Std_RBTree_Std_Data_RBTree___instance__2___rarg___closed__1);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus