chore: update stage0

2022-08-05 23:12:52 -04:00 · 2022-08-05 23:12:52 -04:00 · 3b43cff7d3
commit 3b43cff7d3
parent ab55af01b3
32 changed files with 3274 additions and 1756 deletions
--- a/stage0/src/Init/Core.lean
+++ b/stage0/src/Init/Core.lean
@ -627,6 +627,12 @@ end
 instance [Inhabited α] [Inhabited β] : Inhabited (α × β) where
  default := (default, default)

+instance [Inhabited α] [Inhabited β] : Inhabited (MProd α β) where
+  default := ⟨default, default⟩
+
+instance [Inhabited α] [Inhabited β] : Inhabited (PProd α β) where
+  default := ⟨default, default⟩
+
 instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
  fun (a, b) (a', b') =>
    match decEq a a' with
--- a/stage0/src/Init/Data/Nat/Linear.lean
+++ b/stage0/src/Init/Data/Nat/Linear.lean
@ -338,7 +338,7 @@ theorem Poly.denote_mul (ctx : Context) (k : Nat) (p : Poly) : (p.mul k).denote
  by_cases h : k == 1 <;> simp [h]; simp [eq_of_beq h]
  induction p with
  | nil  => simp
-  | cons kv m ih => cases kv with | mk k' v => simp [ih]
+  | cons kv m ih => cases kv with | _ k' v => simp [ih]

 private theorem eq_of_not_blt_eq_true (h₁ : ¬ (Nat.blt x y = true)) (h₂ : ¬ (Nat.blt y x = true)) : x = y :=
  have h₁ : ¬ x < y := fun h => h₁ (Nat.blt_eq.mpr h)
--- a/stage0/src/Init/Prelude.lean
+++ b/stage0/src/Init/Prelude.lean
@ -380,9 +380,6 @@ set_option linter.unusedVariables.funArgs false in
 /-- Gadget for marking output parameters in type classes. -/
@[reducible] def outParam (α : Sort u) : Sort u := α

-/-- Auxiliary Declaration used to implement the notation (a : α) -/
-@[reducible] def typedExpr (α : Sort u) (a : α) : α := a
-
 set_option linter.unusedVariables.funArgs false in
 /-- Auxiliary Declaration used to implement the named patterns `x@h:p` -/
@[reducible] def namedPattern {α : Sort u} (x a : α) (h : Eq x a) : α := a
--- a/stage0/src/Lean/Data/Lsp/Diagnostics.lean
+++ b/stage0/src/Lean/Data/Lsp/Diagnostics.lean
@ -90,7 +90,7 @@ abbrev Diagnostic := DiagnosticWith String
 structure PublishDiagnosticsParams where
  uri : DocumentUri
  version? : Option Int := none
-  diagnostics: Array Diagnostic
+  diagnostics : Array Diagnostic
  deriving Inhabited, BEq, ToJson, FromJson

 end Lsp
--- a/stage0/src/Lean/Data/Lsp/Extra.lean
+++ b/stage0/src/Lean/Data/Lsp/Extra.lean
@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.

 Authors: Marc Huisinga, Wojciech Nawrocki
 -/
-import Lean.Data.Json
-import Lean.Data.JsonRpc
 import Lean.Data.Lsp.Basic

 /-! This file contains Lean-specific extensions to LSP. See the structures below for which
--- a/stage0/src/Lean/Data/Parsec.lean
+++ b/stage0/src/Lean/Data/Parsec.lean
@ -124,8 +124,8 @@ def digit : Parsec Char := attempt do
 def hexDigit : Parsec Char := attempt do
  let c ← anyChar
  if ('0' ≤ c ∧ c ≤ '9')
-   ∨ ('a' ≤ c ∧ c ≤ 'a')
-   ∨ ('A' ≤ c ∧ c ≤ 'A') then return c else fail s!"hex digit expected"
+   ∨ ('a' ≤ c ∧ c ≤ 'f')
+   ∨ ('A' ≤ c ∧ c ≤ 'F') then return c else fail s!"hex digit expected"

@[inline]
 def asciiLetter : Parsec Char := attempt do
--- a/stage0/src/Lean/Deprecated.lean
+++ b/stage0/src/Lean/Deprecated.lean
@ -24,6 +24,9 @@ builtin_initialize deprecatedAttr : ParametricAttribute (Option Name) ←
 def isDeprecated (env : Environment) (declName : Name) : Bool :=
  Option.isSome <| deprecatedAttr.getParam? env declName

+def MessageData.isDeprecationWarning (msg : MessageData) : Bool :=
+  msg.hasTag (· == ``deprecatedAttr)
+
 def getDeprecatedNewName (env : Environment) (declName : Name) : Option Name :=
  match deprecatedAttr.getParam? env declName with
  | some newName? => newName?
@ -32,7 +35,7 @@ def getDeprecatedNewName (env : Environment) (declName : Name) : Option Name :=
 def checkDeprecated [Monad m] [MonadEnv m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (declName : Name) : m Unit := do
  match deprecatedAttr.getParam? (← getEnv) declName with
  | none => pure ()
-  | some none => logWarning m!"`{declName}` has been deprecated"
-  | some (some newName) => logWarning m!"`{declName}` has been deprecated, use `{newName}` instead"
+  | some none => logWarning <| .tagged ``deprecatedAttr m!"`{declName}` has been deprecated"
+  | some (some newName) => logWarning <| .tagged ``deprecatedAttr m!"`{declName}` has been deprecated, use `{newName}` instead"

 end Lean
--- a/stage0/src/Lean/Elab/Tactic/Conv/Congr.lean
+++ b/stage0/src/Lean/Elab/Tactic/Conv/Congr.lean
@ -137,13 +137,24 @@ def extLetBodyCongr? (mvarId : MVarId) (lhs rhs : Expr) : MetaM (Option MVarId)

 private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId :=
   mvarId.withContext do
-     let userNames := if let some userName := userName? then [userName] else []
     let (lhs, rhs) ← getLhsRhsCore mvarId
-     let lhs ← instantiateMVars lhs
-     if lhs.isForall then
-       let [mvarId, _] ← mvarId.apply (← mkConstWithFreshMVarLevels ``forall_congr) | throwError "'apply forall_congr' unexpected result"
-       let (_, mvarId) ← mvarId.introN 1 userNames
-       markAsConvGoal mvarId
+     let lhs := (← instantiateMVars lhs).cleanupAnnotations
+     if let .forallE n d b bi := lhs then
+       let u ← getLevel d
+       let p : Expr := .lam n d b bi
+       let userName ← if let some userName := userName? then pure userName else mkFreshBinderNameForTactic n
+       let (q, h, mvarNew) ← withLocalDecl userName bi d fun a => do
+         let pa := b.instantiate1 a
+         let (qa, mvarNew) ← mkConvGoalFor pa
+         let q ← mkLambdaFVars #[a] qa
+         let h ← mkLambdaFVars #[a] mvarNew
+         let rhs' ← mkForallFVars #[a] qa
+         unless (← isDefEqGuarded rhs rhs') do
+           throwError "invalid 'ext' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}"
+         return (q, h, mvarNew)
+       let proof := mkApp4 (mkConst ``forall_congr [u]) d p q h
+       mvarId.assign proof
+       return mvarNew.mvarId!
     else if let some mvarId ← extLetBodyCongr? mvarId lhs rhs then
       return mvarId
     else
@ -151,6 +162,7 @@ private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId :
       unless lhsType.isForall do
         throwError "invalid 'ext' conv tactic, function or arrow expected{indentD m!"{lhs} : {lhsType}"}"
       let [mvarId] ← mvarId.apply (← mkConstWithFreshMVarLevels ``funext) | throwError "'apply funext' unexpected result"
+       let userNames := if let some userName := userName? then [userName] else []
       let (_, mvarId) ← mvarId.introN 1 userNames
       markAsConvGoal mvarId

--- a/stage0/src/Lean/Linter/MissingDocs.lean
+++ b/stage0/src/Lean/Linter/MissingDocs.lean
@ -23,6 +23,9 @@ namespace MissingDocs
 abbrev SimpleHandler := Syntax → CommandElabM Unit
 abbrev Handler := Bool → SimpleHandler

+def SimpleHandler.toHandler (h : SimpleHandler) : Handler :=
+  fun enabled stx => if enabled then h stx else pure ()
+
 unsafe def mkHandlerUnsafe (constName : Name) : ImportM Handler := do
  let env  := (← read).env
  let opts := (← read).opts
@ -31,7 +34,7 @@ unsafe def mkHandlerUnsafe (constName : Name) : ImportM Handler := do
  | some info => match info.type with
    | Expr.const ``SimpleHandler _ => do
      let h ← IO.ofExcept $ env.evalConst SimpleHandler opts constName
-      pure fun enabled stx => if enabled then h stx else pure ()
+      pure h.toHandler
    | Expr.const ``Handler _ =>
      IO.ofExcept $ env.evalConst Handler opts constName
    | _ => throw ↑s!"unexpected missing docs handler at '{constName}', `MissingDocs.Handler` or `MissingDocs.SimpleHandler` expected"
@ -39,13 +42,15 @@ unsafe def mkHandlerUnsafe (constName : Name) : ImportM Handler := do
@[implementedBy mkHandlerUnsafe]
 opaque mkHandler (constName : Name) : ImportM Handler

+builtin_initialize builtinHandlersRef : IO.Ref (NameMap Handler) ← IO.mkRef {}
+
 builtin_initialize missingDocsExt :
  PersistentEnvExtension (Name × Name) (Name × Name × Handler) (List (Name × Name) × NameMap Handler) ←
  registerPersistentEnvExtension {
    name            := "missing docs extension"
-    mkInitial       := pure ([], {})
-    addImportedFn   := fun as =>
-      ([], ·) <$> as.foldlM (init := {}) fun s as =>
+    mkInitial       := return ([], ← builtinHandlersRef.get)
+    addImportedFn   := fun as => do
+      ([], ·) <$> as.foldlM (init := ← builtinHandlersRef.get) fun s as =>
        as.foldlM (init := s) fun s (n, k) => s.insert k <$> mkHandler n
    addEntryFn      := fun (entries, s) (n, k, h) => ((n, k)::entries, s.insert k h)
    exportEntriesFn := fun s => s.1.reverse.toArray
@ -63,24 +68,35 @@ partial def missingDocs : Linter := fun stx => do

 builtin_initialize addLinter missingDocs

+def addBuiltinHandler (key : Name) (h : Handler) : IO Unit :=
+  builtinHandlersRef.modify (·.insert key h)
+
 builtin_initialize
-  let name := `missingDocsHandler
-  registerBuiltinAttribute {
+  let mkAttr (builtin : Bool) (name : Name) := registerBuiltinAttribute {
    name
-    descr := "adds a syntax traversal for the missing docs linter"
+    descr           := (if builtin then "(builtin) " else "") ++
+      "adds a syntax traversal for the missing docs linter"
    applicationTime := .afterCompilation
-    add := fun declName stx kind => do
+    add             := fun declName stx kind => do
      unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
      let env ← getEnv
-      unless (env.getModuleIdxFor? declName).isNone do
+      unless builtin || (env.getModuleIdxFor? declName).isNone do
        throwError "invalid attribute '{name}', declaration is in an imported module"
      let decl ← getConstInfo declName
      let fnNameStx ← Attribute.Builtin.getIdent stx
      let key ← Elab.resolveGlobalConstNoOverloadWithInfo fnNameStx
      unless decl.levelParams.isEmpty && (decl.type == .const ``Handler [] || decl.type == .const ``SimpleHandler []) do
        throwError "unexpected missing docs handler at '{declName}', `MissingDocs.Handler` or `MissingDocs.SimpleHandler` expected"
-      setEnv <| missingDocsExt.addEntry env (declName, key, ← mkHandler declName)
+      if builtin then
+        let h := if decl.type == .const ``SimpleHandler [] then
+          mkApp (mkConst ``SimpleHandler.toHandler) (mkConst declName)
+        else mkConst declName
+        declareBuiltin declName <| mkApp2 (mkConst ``addBuiltinHandler) (toExpr key) h
+      else
+        setEnv <| missingDocsExt.addEntry env (declName, key, ← mkHandler declName)
  }
+  mkAttr true `builtinMissingDocsHandler
+  mkAttr false `missingDocsHandler

 def lint (stx : Syntax) (msg : String) : CommandElabM Unit :=
  logWarningAt stx s!"missing doc string for {msg} [linter.missingDocs]"
--- a/stage0/src/Lean/Linter/UnusedVariables.lean
+++ b/stage0/src/Lean/Linter/UnusedVariables.lean
@ -235,7 +235,8 @@ def unusedVariables : Linter := fun cmdStx => do
      continue

    -- publish warning if variable is unused and not ignored
-    publishMessage s!"unused variable `{localDecl.userName}` [linter.unusedVariables]" range
+    publishMessage (.tagged decl_name%
+      m!"unused variable `{localDecl.userName}` [linter.unusedVariables]") range

  return ()
 where
@ -252,4 +253,7 @@ where

 builtin_initialize addLinter unusedVariables

-end Lean.Linter
+end Linter
+
+def MessageData.isUnusedVariableWarning (msg : MessageData) : Bool :=
+  msg.hasTag (· == ``Linter.unusedVariables)
--- a/stage0/src/Lean/Linter/Util.lean
+++ b/stage0/src/Lean/Linter/Util.lean
@ -16,7 +16,7 @@ def getLinterValue (opt : Lean.Option Bool) (o : Options) : Bool := o.get opt.na
 open Lean.Elab Lean.Elab.Command

 def publishMessage
-  (content : String) (range : String.Range) (severity : MessageSeverity := .warning) : CommandElabM Unit :=
+  (content : MessageData) (range : String.Range) (severity : MessageSeverity := .warning) : CommandElabM Unit :=
 do
  let ctx := (← read)
  let messages := (← get).messages |>.add (mkMessageCore ctx.fileName ctx.fileMap content severity range.start range.stop)
--- a/stage0/src/Lean/Log.lean
+++ b/stage0/src/Lean/Log.lean
@ -98,7 +98,7 @@ def logInfo (msgData : MessageData) : m Unit :=
 def logTrace (cls : Name) (msgData : MessageData) : m Unit := do
  logInfo (MessageData.tagged cls m!"[{cls}] {msgData}")

-/-- Log the error message "unknow declaration" -/
+/-- Log the error message "unknown declaration" -/
 def logUnknownDecl (declName : Name) : m Unit :=
  logError m!"unknown declaration '{declName}'"

--- a/stage0/src/Lean/Meta/Tactic/Intro.lean
+++ b/stage0/src/Lean/Meta/Tactic/Intro.lean
@ -72,6 +72,20 @@ register_builtin_option tactic.hygienic : Bool := {
  descr    := "make sure tactics are hygienic"
 }

+private def mkFreshBinderNameForTacticCore (lctx : LocalContext) (binderName : Name) (hygienic := true) : MetaM Name := do
+  if hygienic then
+    mkFreshUserName binderName
+  else
+    return lctx.getUnusedName binderName
+
+/--
+Similar to `mkFreshUserName`, but takes into account `tactic.hygienic` option value.
+If `tactic.hygienic = true`, then the current macro scopes are applied to `binderName`.
+If not, then an unused (accessible) name (based on `binderName`) in the local context is used.
+-/
+def mkFreshBinderNameForTactic (binderName : Name) : MetaM Name := do
+  mkFreshBinderNameForTacticCore (← getLCtx) binderName (tactic.hygienic.get (← getOptions))
+
 private def mkAuxNameImp (preserveBinderNames : Bool) (hygienic : Bool) (useNamesForExplicitOnly : Bool)
    (lctx : LocalContext) (binderName : Name) (isExplicit : Bool) : List Name → MetaM (Name × List Name)
  | []         => mkAuxNameWithoutGivenName []
@ -86,11 +100,9 @@ where
  mkAuxNameWithoutGivenName (rest : List Name) : MetaM (Name × List Name) := do
    if preserveBinderNames then
      return (binderName, rest)
-    else if hygienic then
-      let binderName ← mkFreshUserName binderName
-      return (binderName, rest)
    else
-      return (lctx.getUnusedName binderName, rest)
+      let binderName ← mkFreshBinderNameForTacticCore lctx binderName hygienic
+      return (binderName, rest)

 def introNCore (mvarId : MVarId) (n : Nat) (givenNames : List Name) (useNamesForExplicitOnly : Bool) (preserveBinderNames : Bool)
    : MetaM (Array FVarId × MVarId) := do
--- a/stage0/src/Lean/Server/InfoUtils.lean
+++ b/stage0/src/Lean/Server/InfoUtils.lean
@ -4,10 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.

 Authors: Wojciech Nawrocki
 -/
-import Lean.DocString
-import Lean.Elab.InfoTree
 import Lean.PrettyPrinter
-import Lean.Util.Sorry

 protected structure String.Range where
  start : String.Pos
--- a/stage0/src/Lean/Server/References.lean
+++ b/stage0/src/Lean/Server/References.lean
@ -4,14 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.

 Authors: Joscha Mennicken
 -/
-
-import Init.System.IO
-import Lean.Data.Json
-import Lean.Data.Lsp
-
 import Lean.Server.Utils
-import Lean.Server.InfoUtils
-import Lean.Server.Snapshots

 /-! # Representing collected and deduplicated definitions and usages -/

--- a/stage0/src/Lean/Widget/InteractiveDiagnostic.lean
+++ b/stage0/src/Lean/Widget/InteractiveDiagnostic.lean
@ -4,16 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.

 Authors: Wojciech Nawrocki
 -/
-import Lean.Data.Lsp
-import Lean.Message
-import Lean.Elab.InfoTree
-
+import Lean.Linter.UnusedVariables
 import Lean.Server.Utils
-import Lean.Server.Rpc.Basic
-
-import Lean.Widget.Basic
-import Lean.Widget.TaggedText
-import Lean.Widget.InteractiveCode
 import Lean.Widget.InteractiveGoal

 namespace Lean.Widget
@ -160,21 +152,19 @@ def msgToInteractiveDiagnostic (text : FileMap) (m : Message) (hasWidgets : Bool
    | none        => low
  let range : Range := ⟨low, high⟩
  let fullRange : Range := ⟨low, fullHigh⟩
-  let severity := match m.severity with
-    | MessageSeverity.information => DiagnosticSeverity.information
-    | MessageSeverity.warning     => DiagnosticSeverity.warning
-    | MessageSeverity.error       => DiagnosticSeverity.error
-  let source := "Lean 4"
+  let severity? := some <| match m.severity with
+    | .information => .information
+    | .warning     => .warning
+    | .error       => .error
+  let source? := some "Lean 4"
+  let tags? :=
+    if m.data.isDeprecationWarning then some #[.deprecated]
+    else if m.data.isUnusedVariableWarning then some #[.unnecessary]
+    else none
  let message ← try
      msgToInteractive m.data hasWidgets
    catch ex =>
      pure <| TaggedText.text s!"[error when printing message: {ex.toString}]"
-  pure {
-    range := range
-    fullRange := fullRange
-    severity? := severity
-    source? := source
-    message := message
-  }
+  pure { range, fullRange, severity?, source?, message, tags? }

 end Lean.Widget
--- a/stage0/stdlib/Init/Core.c
+++ b/stage0/stdlib/Init/Core.c
@ -24,6 +24,7 @@ LEAN_EXPORT lean_object* l_instInhabitedTask___rarg(lean_object*);
 LEAN_EXPORT lean_object* l_term___u2194__;
 LEAN_EXPORT lean_object* l_Quotient_hrecOn___rarg(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Quotient_lift(lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_instInhabitedMProd___rarg(lean_object*, lean_object*);
 LEAN_EXPORT uint8_t l_instDecidableEqProp___rarg(uint8_t);
 LEAN_EXPORT uint8_t l_Lean_reduceBool(uint8_t);
 LEAN_EXPORT lean_object* l_inline(lean_object*);
@ -132,6 +133,7 @@ static lean_object* l___aux__Init__Core______macroRules__term___u2295____1___clo
 LEAN_EXPORT lean_object* l_toBoolUsing___rarg___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_strictOr___boxed(lean_object*, lean_object*);
 static lean_object* l___aux__Init__Core______macroRules__term___x21_x3d____1___closed__4;
+LEAN_EXPORT lean_object* l_instInhabitedPProd(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Subtype_instDecidableEqSubtype___rarg(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_instInhabitedForInStep__1(lean_object*);
 static lean_object* l_term___x3c_x2d_x3e_____closed__6;
@ -191,6 +193,7 @@ LEAN_EXPORT lean_object* l_Quotient_mk_x27___rarg___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_term___u2260__;
 LEAN_EXPORT lean_object* l_Quotient_hrecOn___boxed(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Quotient_rec(lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_instInhabitedPProd___rarg(lean_object*, lean_object*);
 static lean_object* l___aux__Init__Core______macroRules__term___x3c_x2d_x3e____1___closed__2;
 static lean_object* l___aux__Init__Core______macroRules__term_x7b_x7d__1___closed__3;
 LEAN_EXPORT lean_object* l___aux__Init__Core______unexpand__bne__1(lean_object*, lean_object*, lean_object*);
@ -309,6 +312,7 @@ LEAN_EXPORT lean_object* l_Thunk_bind___rarg___lambda__1(lean_object*, lean_obje
 LEAN_EXPORT lean_object* l___aux__Init__Core______unexpand__Ne__1___boxed(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Eq_ndrecOn___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_term___u2248_____closed__1;
+LEAN_EXPORT lean_object* l_instInhabitedMProd(lean_object*, lean_object*);
 static lean_object* l_term___u2295_____closed__3;
 LEAN_EXPORT lean_object* l_Quotient_rec___rarg(lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
@ -5891,6 +5895,42 @@ x_3 = lean_alloc_closure((void*)(l_instInhabitedProd___rarg), 2, 0);
 return x_3;
 }
 }
+LEAN_EXPORT lean_object* l_instInhabitedMProd___rarg(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_3, 0, x_1);
+lean_ctor_set(x_3, 1, x_2);
+return x_3;
+}
+}
+LEAN_EXPORT lean_object* l_instInhabitedMProd(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = lean_alloc_closure((void*)(l_instInhabitedMProd___rarg), 2, 0);
+return x_3;
+}
+}
+LEAN_EXPORT lean_object* l_instInhabitedPProd___rarg(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_3, 0, x_1);
+lean_ctor_set(x_3, 1, x_2);
+return x_3;
+}
+}
+LEAN_EXPORT lean_object* l_instInhabitedPProd(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = lean_alloc_closure((void*)(l_instInhabitedPProd___rarg), 2, 0);
+return x_3;
+}
+}
 LEAN_EXPORT lean_object* l_instDecidableEqProd___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
--- a/stage0/stdlib/Init/Prelude.c
+++ b/stage0/stdlib/Init/Prelude.c
@ -356,7 +356,6 @@ LEAN_EXPORT lean_object* l_instInhabited___rarg(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_UInt32_decLt___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_UInt32_toNat___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_reservedMacroScope;
-LEAN_EXPORT lean_object* l_typedExpr___rarg___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Macro_instMonadRefMacroM;
 LEAN_EXPORT lean_object* l_instLEFin(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Macro_throwError(lean_object*);
@ -452,7 +451,6 @@ LEAN_EXPORT lean_object* l_instMonadReader___rarg(lean_object*);
 LEAN_EXPORT lean_object* l_instMonadReaderOfReaderT(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_instInhabitedSyntax;
 LEAN_EXPORT lean_object* l_Lean_firstFrontendMacroScope;
-LEAN_EXPORT lean_object* l_typedExpr(lean_object*);
 LEAN_EXPORT lean_object* l_instHDiv(lean_object*);
 LEAN_EXPORT lean_object* l_Substring_bsize(lean_object*);
 LEAN_EXPORT lean_object* l_List_set___rarg(lean_object*, lean_object*, lean_object*);
@ -515,7 +513,6 @@ LEAN_EXPORT lean_object* l_instLEUInt32;
 LEAN_EXPORT lean_object* l_instDecidableEqChar___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_instTransEq___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_UInt16_decEq___boxed(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_typedExpr___rarg(lean_object*);
 static lean_object* l_Lean_nullKind___closed__2;
 LEAN_EXPORT lean_object* l_Lean_Syntax_matchesIdent___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_MonadExcept_instOrElse(lean_object*, lean_object*);
@ -1081,30 +1078,6 @@ lean_dec(x_1);
 return x_2;
 }
 }
-LEAN_EXPORT lean_object* l_typedExpr___rarg(lean_object* x_1) {
-_start:
-{
-lean_inc(x_1);
-return x_1;
-}
-}
-LEAN_EXPORT lean_object* l_typedExpr(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_typedExpr___rarg___boxed), 1, 0);
-return x_2;
-}
-}
-LEAN_EXPORT lean_object* l_typedExpr___rarg___boxed(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = l_typedExpr___rarg(x_1);
-lean_dec(x_1);
-return x_2;
-}
-}
 LEAN_EXPORT lean_object* l_namedPattern___rarg(lean_object* x_1, lean_object* x_2) {
 _start:
 {
--- a/stage0/stdlib/Lean/Data/Lsp/Extra.c
+++ b/stage0/stdlib/Lean/Data/Lsp/Extra.c
@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Lean.Data.Lsp.Extra
-// Imports: Init Lean.Data.Json Lean.Data.JsonRpc Lean.Data.Lsp.Basic
+// Imports: Init Lean.Data.Lsp.Basic
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@ -4554,8 +4554,6 @@ return x_1;
 }
 }
 lean_object* initialize_Init(uint8_t builtin, lean_object*);
-lean_object* initialize_Lean_Data_Json(uint8_t builtin, lean_object*);
-lean_object* initialize_Lean_Data_JsonRpc(uint8_t builtin, lean_object*);
 lean_object* initialize_Lean_Data_Lsp_Basic(uint8_t builtin, lean_object*);
 static bool _G_initialized = false;
 LEAN_EXPORT lean_object* initialize_Lean_Data_Lsp_Extra(uint8_t builtin, lean_object* w) {
@ -4565,12 +4563,6 @@ _G_initialized = true;
 res = initialize_Init(builtin, lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-res = initialize_Lean_Data_Json(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-res = initialize_Lean_Data_JsonRpc(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
 res = initialize_Lean_Data_Lsp_Basic(builtin, lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
--- a/stage0/stdlib/Lean/Data/Parsec.c
+++ b/stage0/stdlib/Lean/Data/Parsec.c
@ -2392,43 +2392,43 @@ return x_4;
 }
 else
 {
-lean_object* x_5; uint32_t x_6; lean_object* x_7; uint32_t x_32; uint8_t x_33; 
+lean_object* x_5; uint32_t x_6; lean_object* x_7; uint32_t x_35; uint8_t x_36; 
 lean_inc(x_1);
 x_5 = l_String_Iterator_next(x_1);
 x_6 = l_String_Iterator_curr(x_1);
-x_32 = 48;
-x_33 = lean_uint32_dec_le(x_32, x_6);
-if (x_33 == 0)
-{
-lean_object* x_34; 
-x_34 = lean_box(0);
-x_7 = x_34;
-goto block_31;
-}
-else
-{
-uint32_t x_35; uint8_t x_36; 
-x_35 = 57;
-x_36 = lean_uint32_dec_le(x_6, x_35);
+x_35 = 48;
+x_36 = lean_uint32_dec_le(x_35, x_6);
 if (x_36 == 0)
 {
 lean_object* x_37; 
 x_37 = lean_box(0);
 x_7 = x_37;
-goto block_31;
+goto block_34;
 }
 else
 {
-lean_object* x_38; lean_object* x_39; 
+uint32_t x_38; uint8_t x_39; 
+x_38 = 57;
+x_39 = lean_uint32_dec_le(x_6, x_38);
+if (x_39 == 0)
+{
+lean_object* x_40; 
+x_40 = lean_box(0);
+x_7 = x_40;
+goto block_34;
+}
+else
+{
+lean_object* x_41; lean_object* x_42; 
 lean_dec(x_1);
-x_38 = lean_box_uint32(x_6);
-x_39 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_39, 0, x_5);
-lean_ctor_set(x_39, 1, x_38);
-return x_39;
+x_41 = lean_box_uint32(x_6);
+x_42 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_42, 0, x_5);
+lean_ctor_set(x_42, 1, x_41);
+return x_42;
 }
 }
-block_31:
+block_34:
 {
 uint32_t x_8; uint8_t x_9; 
 lean_dec(x_7);
@ -2451,84 +2451,87 @@ return x_13;
 }
 else
 {
-uint8_t x_14; 
-x_14 = lean_uint32_dec_le(x_6, x_10);
-if (x_14 == 0)
+uint32_t x_14; uint8_t x_15; 
+x_14 = 70;
+x_15 = lean_uint32_dec_le(x_6, x_14);
+if (x_15 == 0)
 {
-lean_object* x_15; lean_object* x_16; 
+lean_object* x_16; lean_object* x_17; 
 lean_dec(x_5);
-x_15 = l_Lean_Parsec_hexDigit___closed__1;
-x_16 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_16, 0, x_1);
-lean_ctor_set(x_16, 1, x_15);
-return x_16;
+x_16 = l_Lean_Parsec_hexDigit___closed__1;
+x_17 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_17, 0, x_1);
+lean_ctor_set(x_17, 1, x_16);
+return x_17;
 }
 else
 {
-lean_object* x_17; lean_object* x_18; 
+lean_object* x_18; lean_object* x_19; 
 lean_dec(x_1);
-x_17 = lean_box_uint32(x_6);
-x_18 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_18, 0, x_5);
-lean_ctor_set(x_18, 1, x_17);
-return x_18;
+x_18 = lean_box_uint32(x_6);
+x_19 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_19, 0, x_5);
+lean_ctor_set(x_19, 1, x_18);
+return x_19;
 }
 }
 }
 else
 {
-uint8_t x_19; 
-x_19 = lean_uint32_dec_le(x_6, x_8);
-if (x_19 == 0)
-{
 uint32_t x_20; uint8_t x_21; 
-x_20 = 65;
-x_21 = lean_uint32_dec_le(x_20, x_6);
+x_20 = 102;
+x_21 = lean_uint32_dec_le(x_6, x_20);
 if (x_21 == 0)
 {
-lean_object* x_22; lean_object* x_23; 
+uint32_t x_22; uint8_t x_23; 
+x_22 = 65;
+x_23 = lean_uint32_dec_le(x_22, x_6);
+if (x_23 == 0)
+{
+lean_object* x_24; lean_object* x_25; 
 lean_dec(x_5);
-x_22 = l_Lean_Parsec_hexDigit___closed__1;
-x_23 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_23, 0, x_1);
-lean_ctor_set(x_23, 1, x_22);
-return x_23;
+x_24 = l_Lean_Parsec_hexDigit___closed__1;
+x_25 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_25, 0, x_1);
+lean_ctor_set(x_25, 1, x_24);
+return x_25;
 }
 else
 {
-uint8_t x_24; 
-x_24 = lean_uint32_dec_le(x_6, x_20);
-if (x_24 == 0)
+uint32_t x_26; uint8_t x_27; 
+x_26 = 70;
+x_27 = lean_uint32_dec_le(x_6, x_26);
+if (x_27 == 0)
 {
-lean_object* x_25; lean_object* x_26; 
+lean_object* x_28; lean_object* x_29; 
 lean_dec(x_5);
-x_25 = l_Lean_Parsec_hexDigit___closed__1;
-x_26 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_26, 0, x_1);
-lean_ctor_set(x_26, 1, x_25);
-return x_26;
+x_28 = l_Lean_Parsec_hexDigit___closed__1;
+x_29 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_29, 0, x_1);
+lean_ctor_set(x_29, 1, x_28);
+return x_29;
 }
 else
 {
-lean_object* x_27; lean_object* x_28; 
+lean_object* x_30; lean_object* x_31; 
 lean_dec(x_1);
-x_27 = lean_box_uint32(x_6);
-x_28 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_28, 0, x_5);
-lean_ctor_set(x_28, 1, x_27);
-return x_28;
+x_30 = lean_box_uint32(x_6);
+x_31 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_31, 0, x_5);
+lean_ctor_set(x_31, 1, x_30);
+return x_31;
 }
 }
 }
 else
 {
-lean_object* x_29; lean_object* x_30; 
+lean_object* x_32; lean_object* x_33; 
 lean_dec(x_1);
-x_29 = lean_box_uint32(x_6);
-x_30 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_30, 0, x_5);
-lean_ctor_set(x_30, 1, x_29);
-return x_30;
+x_32 = lean_box_uint32(x_6);
+x_33 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_33, 0, x_5);
+lean_ctor_set(x_33, 1, x_32);
+return x_33;
 }
 }
 }
--- a/stage0/stdlib/Lean/Data/Xml/Parser.c
+++ b/stage0/stdlib/Lean/Data/Xml/Parser.c
@ -16292,30 +16292,30 @@ return x_41;
 }
 else
 {
-lean_object* x_42; uint32_t x_43; lean_object* x_44; uint32_t x_63; uint8_t x_64; 
+lean_object* x_42; uint32_t x_43; lean_object* x_44; uint32_t x_66; uint8_t x_67; 
 lean_inc(x_1);
 x_42 = l_String_Iterator_next(x_1);
 x_43 = l_String_Iterator_curr(x_1);
-x_63 = 48;
-x_64 = lean_uint32_dec_le(x_63, x_43);
-if (x_64 == 0)
-{
-lean_object* x_65; 
-x_65 = lean_box(0);
-x_44 = x_65;
-goto block_62;
-}
-else
-{
-uint32_t x_66; uint8_t x_67; 
-x_66 = 57;
-x_67 = lean_uint32_dec_le(x_43, x_66);
+x_66 = 48;
+x_67 = lean_uint32_dec_le(x_66, x_43);
 if (x_67 == 0)
 {
 lean_object* x_68; 
 x_68 = lean_box(0);
 x_44 = x_68;
-goto block_62;
+goto block_65;
+}
+else
+{
+uint32_t x_69; uint8_t x_70; 
+x_69 = 57;
+x_70 = lean_uint32_dec_le(x_43, x_69);
+if (x_70 == 0)
+{
+lean_object* x_71; 
+x_71 = lean_box(0);
+x_44 = x_71;
+goto block_65;
 }
 else
 {
@ -16325,7 +16325,7 @@ x_3 = x_43;
 goto block_38;
 }
 }
-block_62:
+block_65:
 {
 uint32_t x_45; uint8_t x_46; 
 lean_dec(x_44);
@ -16348,17 +16348,18 @@ return x_50;
 }
 else
 {
-uint8_t x_51; 
-x_51 = lean_uint32_dec_le(x_43, x_47);
-if (x_51 == 0)
+uint32_t x_51; uint8_t x_52; 
+x_51 = 70;
+x_52 = lean_uint32_dec_le(x_43, x_51);
+if (x_52 == 0)
 {
-lean_object* x_52; lean_object* x_53; 
+lean_object* x_53; lean_object* x_54; 
 lean_dec(x_42);
-x_52 = l_Lean_Xml_Parser_CharRef___lambda__2___closed__1;
-x_53 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_53, 0, x_1);
-lean_ctor_set(x_53, 1, x_52);
-return x_53;
+x_53 = l_Lean_Xml_Parser_CharRef___lambda__2___closed__1;
+x_54 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_54, 0, x_1);
+lean_ctor_set(x_54, 1, x_53);
+return x_54;
 }
 else
 {
@ -16371,36 +16372,38 @@ goto block_38;
 }
 else
 {
-uint8_t x_54; 
-x_54 = lean_uint32_dec_le(x_43, x_45);
-if (x_54 == 0)
-{
 uint32_t x_55; uint8_t x_56; 
-x_55 = 65;
-x_56 = lean_uint32_dec_le(x_55, x_43);
+x_55 = 102;
+x_56 = lean_uint32_dec_le(x_43, x_55);
 if (x_56 == 0)
 {
-lean_object* x_57; lean_object* x_58; 
+uint32_t x_57; uint8_t x_58; 
+x_57 = 65;
+x_58 = lean_uint32_dec_le(x_57, x_43);
+if (x_58 == 0)
+{
+lean_object* x_59; lean_object* x_60; 
 lean_dec(x_42);
-x_57 = l_Lean_Xml_Parser_CharRef___lambda__2___closed__1;
-x_58 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_58, 0, x_1);
-lean_ctor_set(x_58, 1, x_57);
-return x_58;
+x_59 = l_Lean_Xml_Parser_CharRef___lambda__2___closed__1;
+x_60 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_60, 0, x_1);
+lean_ctor_set(x_60, 1, x_59);
+return x_60;
 }
 else
 {
-uint8_t x_59; 
-x_59 = lean_uint32_dec_le(x_43, x_55);
-if (x_59 == 0)
+uint32_t x_61; uint8_t x_62; 
+x_61 = 70;
+x_62 = lean_uint32_dec_le(x_43, x_61);
+if (x_62 == 0)
 {
-lean_object* x_60; lean_object* x_61; 
+lean_object* x_63; lean_object* x_64; 
 lean_dec(x_42);
-x_60 = l_Lean_Xml_Parser_CharRef___lambda__2___closed__1;
-x_61 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_61, 0, x_1);
-lean_ctor_set(x_61, 1, x_60);
-return x_61;
+x_63 = l_Lean_Xml_Parser_CharRef___lambda__2___closed__1;
+x_64 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_64, 0, x_1);
+lean_ctor_set(x_64, 1, x_63);
+return x_64;
 }
 else
 {
--- a/stage0/stdlib/Lean/Deprecated.c
+++ b/stage0/stdlib/Lean/Deprecated.c
@ -13,6 +13,8 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
+LEAN_EXPORT uint8_t l_Lean_MessageData_isDeprecationWarning(lean_object*);
+static lean_object* l_Lean_MessageData_isDeprecationWarning___closed__1;
 lean_object* l_Lean_addMessageContextPartial___at_Lean_Core_instAddMessageContextCoreM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_initFn____x40_Lean_Deprecated___hyg_4____spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_resolveGlobalConstCore___at_Lean_initFn____x40_Lean_Deprecated___hyg_4____spec__6___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -27,12 +29,14 @@ LEAN_EXPORT lean_object* l_Lean_deprecatedAttr;
 static lean_object* l_Lean_initFn____x40_Lean_Deprecated___hyg_4____closed__6;
 LEAN_EXPORT lean_object* l_Lean_resolveGlobalConst___at_Lean_initFn____x40_Lean_Deprecated___hyg_4____spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_mapTRAux___at_Lean_resolveGlobalConstCore___spec__2(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_MessageData_isDeprecationWarning___boxed(lean_object*);
 extern lean_object* l_Std_Format_defWidth;
 LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Deprecated___hyg_4____lambda__4___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_List_filterMap___at_Lean_resolveGlobalConst___spec__1(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_initFn____x40_Lean_Deprecated___hyg_4____spec__10(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_initFn____x40_Lean_Deprecated___hyg_4____closed__4;
 lean_object* lean_st_ref_get(lean_object*, lean_object*);
+uint8_t lean_name_eq(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Deprecated___hyg_4____lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_logWarning___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_initFn____x40_Lean_Deprecated___hyg_4____closed__1;
@ -46,6 +50,7 @@ static lean_object* l_Lean_checkDeprecated___rarg___lambda__1___closed__3;
 static lean_object* l_Lean_checkDeprecated___rarg___lambda__1___closed__4;
 static lean_object* l_Lean_throwUnknownConstant___at_Lean_initFn____x40_Lean_Deprecated___hyg_4____spec__8___closed__3;
 lean_object* l_List_mapTRAux___at_Lean_resolveGlobalConstNoOverload___spec__1(lean_object*, lean_object*);
+uint8_t l_Lean_MessageData_hasTag(lean_object*, lean_object*);
 static lean_object* l_Lean_initFn____x40_Lean_Deprecated___hyg_4____closed__7;
 LEAN_EXPORT lean_object* l_Lean_checkDeprecated___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_ParametricAttribute_getParam_x3f___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -89,6 +94,8 @@ lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_isDeprecated___boxed(lean_object*, lean_object*);
 static lean_object* l_Lean_initFn____x40_Lean_Deprecated___hyg_4____closed__2;
 static lean_object* l_Lean_isDeprecated___closed__1;
+LEAN_EXPORT lean_object* l_Lean_MessageData_isDeprecationWarning___lambda__1___boxed(lean_object*);
+LEAN_EXPORT uint8_t l_Lean_MessageData_isDeprecationWarning___lambda__1(lean_object*);
 uint8_t l_List_isEmpty___rarg(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_initFn____x40_Lean_Deprecated___hyg_4____spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_toString___at_Lean_resolveGlobalConstNoOverloadCore___spec__2(lean_object*);
@ -1291,6 +1298,51 @@ x_4 = lean_box(x_3);
 return x_4;
 }
 }
+LEAN_EXPORT uint8_t l_Lean_MessageData_isDeprecationWarning___lambda__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; uint8_t x_3; 
+x_2 = l_Lean_initFn____x40_Lean_Deprecated___hyg_4____closed__4;
+x_3 = lean_name_eq(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l_Lean_MessageData_isDeprecationWarning___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_MessageData_isDeprecationWarning___lambda__1___boxed), 1, 0);
+return x_1;
+}
+}
+LEAN_EXPORT uint8_t l_Lean_MessageData_isDeprecationWarning(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; uint8_t x_3; 
+x_2 = l_Lean_MessageData_isDeprecationWarning___closed__1;
+x_3 = l_Lean_MessageData_hasTag(x_2, x_1);
+return x_3;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_MessageData_isDeprecationWarning___lambda__1___boxed(lean_object* x_1) {
+_start:
+{
+uint8_t x_2; lean_object* x_3; 
+x_2 = l_Lean_MessageData_isDeprecationWarning___lambda__1(x_1);
+lean_dec(x_1);
+x_3 = lean_box(x_2);
+return x_3;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_MessageData_isDeprecationWarning___boxed(lean_object* x_1) {
+_start:
+{
+uint8_t x_2; lean_object* x_3; 
+x_2 = l_Lean_MessageData_isDeprecationWarning(x_1);
+x_3 = lean_box(x_2);
+return x_3;
+}
+}
 LEAN_EXPORT lean_object* l_Lean_getDeprecatedNewName(lean_object* x_1, lean_object* x_2) {
 _start:
 {
@ -1415,7 +1467,7 @@ lean_inc(x_14);
 lean_dec(x_9);
 if (lean_obj_tag(x_14) == 0)
 {
-lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; 
+lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; 
 x_15 = lean_alloc_ctor(4, 1, 0);
 lean_ctor_set(x_15, 0, x_1);
 x_16 = l_Lean_checkDeprecated___rarg___lambda__1___closed__2;
@ -1426,36 +1478,44 @@ x_18 = l_Lean_checkDeprecated___rarg___lambda__1___closed__4;
 x_19 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_19, 0, x_17);
 lean_ctor_set(x_19, 1, x_18);
-x_20 = l_Lean_logWarning___rarg(x_2, x_3, x_4, x_5, x_19);
-return x_20;
+x_20 = l_Lean_initFn____x40_Lean_Deprecated___hyg_4____closed__4;
+x_21 = lean_alloc_ctor(11, 2, 0);
+lean_ctor_set(x_21, 0, x_20);
+lean_ctor_set(x_21, 1, x_19);
+x_22 = l_Lean_logWarning___rarg(x_2, x_3, x_4, x_5, x_21);
+return x_22;
 }
 else
 {
-lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; 
-x_21 = lean_ctor_get(x_14, 0);
-lean_inc(x_21);
+lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; 
+x_23 = lean_ctor_get(x_14, 0);
+lean_inc(x_23);
 lean_dec(x_14);
-x_22 = lean_alloc_ctor(4, 1, 0);
-lean_ctor_set(x_22, 0, x_1);
-x_23 = l_Lean_checkDeprecated___rarg___lambda__1___closed__2;
-x_24 = lean_alloc_ctor(10, 2, 0);
-lean_ctor_set(x_24, 0, x_23);
-lean_ctor_set(x_24, 1, x_22);
-x_25 = l_Lean_checkDeprecated___rarg___lambda__1___closed__6;
+x_24 = lean_alloc_ctor(4, 1, 0);
+lean_ctor_set(x_24, 0, x_1);
+x_25 = l_Lean_checkDeprecated___rarg___lambda__1___closed__2;
 x_26 = lean_alloc_ctor(10, 2, 0);
-lean_ctor_set(x_26, 0, x_24);
-lean_ctor_set(x_26, 1, x_25);
-x_27 = lean_alloc_ctor(4, 1, 0);
-lean_ctor_set(x_27, 0, x_21);
+lean_ctor_set(x_26, 0, x_25);
+lean_ctor_set(x_26, 1, x_24);
+x_27 = l_Lean_checkDeprecated___rarg___lambda__1___closed__6;
 x_28 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_28, 0, x_26);
 lean_ctor_set(x_28, 1, x_27);
-x_29 = l_Lean_checkDeprecated___rarg___lambda__1___closed__8;
+x_29 = lean_alloc_ctor(4, 1, 0);
+lean_ctor_set(x_29, 0, x_23);
 x_30 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_30, 0, x_28);
 lean_ctor_set(x_30, 1, x_29);
-x_31 = l_Lean_logWarning___rarg(x_2, x_3, x_4, x_5, x_30);
-return x_31;
+x_31 = l_Lean_checkDeprecated___rarg___lambda__1___closed__8;
+x_32 = lean_alloc_ctor(10, 2, 0);
+lean_ctor_set(x_32, 0, x_30);
+lean_ctor_set(x_32, 1, x_31);
+x_33 = l_Lean_initFn____x40_Lean_Deprecated___hyg_4____closed__4;
+x_34 = lean_alloc_ctor(11, 2, 0);
+lean_ctor_set(x_34, 0, x_33);
+lean_ctor_set(x_34, 1, x_32);
+x_35 = l_Lean_logWarning___rarg(x_2, x_3, x_4, x_5, x_34);
+return x_35;
 }
 }
 }
@ -1555,6 +1615,8 @@ lean_mark_persistent(l_Lean_deprecatedAttr);
 lean_dec_ref(res);
 }l_Lean_isDeprecated___closed__1 = _init_l_Lean_isDeprecated___closed__1();
 lean_mark_persistent(l_Lean_isDeprecated___closed__1);
+l_Lean_MessageData_isDeprecationWarning___closed__1 = _init_l_Lean_MessageData_isDeprecationWarning___closed__1();
+lean_mark_persistent(l_Lean_MessageData_isDeprecationWarning___closed__1);
 l_Lean_checkDeprecated___rarg___lambda__1___closed__1 = _init_l_Lean_checkDeprecated___rarg___lambda__1___closed__1();
 lean_mark_persistent(l_Lean_checkDeprecated___rarg___lambda__1___closed__1);
 l_Lean_checkDeprecated___rarg___lambda__1___closed__2 = _init_l_Lean_checkDeprecated___rarg___lambda__1___closed__2();
--- a/stage0/stdlib/Lean/Elab/Tactic/Conv/Congr.c
+++ b/stage0/stdlib/Lean/Elab/Tactic/Conv/Congr.c
--- a/stage0/stdlib/Lean/Elab/Term.c
+++ b/stage0/stdlib/Lean/Elab/Term.c
@ -24,6 +24,7 @@ LEAN_EXPORT lean_object* l_Lean_getConstInfo___at_Lean_Elab_Term_mkConst___spec_
 LEAN_EXPORT lean_object* l_Lean_Elab_withoutModifyingStateWithInfoAndMessages(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_ContextInfo_save___at_Lean_Elab_Term_withoutModifyingElabMetaStateWithInfo___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_Tactic_instInhabitedSnapshot___closed__25;
+static lean_object* l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__10;
 LEAN_EXPORT lean_object* l_Lean_Elab_Term_instMonadMacroAdapterTermElabM;
 static lean_object* l_Lean_Elab_throwAutoBoundImplicitLocal___at_Lean_Elab_Term_resolveName_process___spec__1___closed__1;
 static lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_isExplicitApp___closed__1;
@ -1495,6 +1496,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_withSaveInfoContext___at_Lean_Elab_Term_wit
 static lean_object* l_Lean_logTrace___at_Lean_Elab_Term_traceAtCmdPos___spec__1___closed__4;
 static lean_object* l_Lean_Elab_ContextInfo_saveNoFileMap___at_Lean_Elab_Term_withoutModifyingElabMetaStateWithInfo___spec__4___rarg___closed__2;
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
+static lean_object* l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__11;
 static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5877____closed__1;
 LEAN_EXPORT lean_object* l_Lean_localDeclDependsOn___at_Lean_Elab_Term_addAutoBoundImplicits_go___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Term_ContainsPendingMVar_visit___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -57060,24 +57062,25 @@ static lean_object* _init_l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string_from_bytes("`", 1);
+x_1 = lean_mk_string_from_bytes("deprecatedAttr", 14);
 return x_1;
 }
 }
 static lean_object* _init_l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__3() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__2;
-x_2 = l_Lean_stringToMessageData(x_1);
-return x_2;
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Elab_Term_mkTermElabAttributeUnsafe___closed__2;
+x_2 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__2;
+x_3 = l_Lean_Name_str___override(x_1, x_2);
+return x_3;
 }
 }
 static lean_object* _init_l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__4() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string_from_bytes("` has been deprecated", 21);
+x_1 = lean_mk_string_from_bytes("`", 1);
 return x_1;
 }
 }
@ -57094,7 +57097,7 @@ static lean_object* _init_l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string_from_bytes("` has been deprecated, use `", 28);
+x_1 = lean_mk_string_from_bytes("` has been deprecated", 21);
 return x_1;
 }
 }
@ -57111,7 +57114,7 @@ static lean_object* _init_l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string_from_bytes("` instead", 9);
+x_1 = lean_mk_string_from_bytes("` has been deprecated, use `", 28);
 return x_1;
 }
 }
@ -57124,6 +57127,23 @@ x_2 = l_Lean_stringToMessageData(x_1);
 return x_2;
 }
 }
+static lean_object* _init_l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__10() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string_from_bytes("` instead", 9);
+return x_1;
+}
+}
+static lean_object* _init_l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__11() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__10;
+x_2 = l_Lean_stringToMessageData(x_1);
+return x_2;
+}
+}
 LEAN_EXPORT lean_object* l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
 _start:
 {
@ -57165,68 +57185,76 @@ lean_inc(x_18);
 lean_dec(x_16);
 if (lean_obj_tag(x_18) == 0)
 {
-lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; 
+lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; 
 x_19 = lean_alloc_ctor(4, 1, 0);
 lean_ctor_set(x_19, 0, x_1);
-x_20 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__3;
+x_20 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__5;
 x_21 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_21, 0, x_20);
 lean_ctor_set(x_21, 1, x_19);
-x_22 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__5;
+x_22 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__7;
 x_23 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_23, 0, x_21);
 lean_ctor_set(x_23, 1, x_22);
-x_24 = l_Lean_logWarning___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__2(x_23, x_2, x_3, x_4, x_5, x_6, x_7, x_12);
-return x_24;
+x_24 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__3;
+x_25 = lean_alloc_ctor(11, 2, 0);
+lean_ctor_set(x_25, 0, x_24);
+lean_ctor_set(x_25, 1, x_23);
+x_26 = l_Lean_logWarning___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__2(x_25, x_2, x_3, x_4, x_5, x_6, x_7, x_12);
+return x_26;
 }
 else
 {
-lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; 
-x_25 = lean_ctor_get(x_18, 0);
-lean_inc(x_25);
+lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; 
+x_27 = lean_ctor_get(x_18, 0);
+lean_inc(x_27);
 lean_dec(x_18);
-x_26 = lean_alloc_ctor(4, 1, 0);
-lean_ctor_set(x_26, 0, x_1);
-x_27 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__3;
-x_28 = lean_alloc_ctor(10, 2, 0);
-lean_ctor_set(x_28, 0, x_27);
-lean_ctor_set(x_28, 1, x_26);
-x_29 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__7;
+x_28 = lean_alloc_ctor(4, 1, 0);
+lean_ctor_set(x_28, 0, x_1);
+x_29 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__5;
 x_30 = lean_alloc_ctor(10, 2, 0);
-lean_ctor_set(x_30, 0, x_28);
-lean_ctor_set(x_30, 1, x_29);
-x_31 = lean_alloc_ctor(4, 1, 0);
-lean_ctor_set(x_31, 0, x_25);
+lean_ctor_set(x_30, 0, x_29);
+lean_ctor_set(x_30, 1, x_28);
+x_31 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__9;
 x_32 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_32, 0, x_30);
 lean_ctor_set(x_32, 1, x_31);
-x_33 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__9;
+x_33 = lean_alloc_ctor(4, 1, 0);
+lean_ctor_set(x_33, 0, x_27);
 x_34 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_34, 0, x_32);
 lean_ctor_set(x_34, 1, x_33);
-x_35 = l_Lean_logWarning___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__2(x_34, x_2, x_3, x_4, x_5, x_6, x_7, x_12);
-return x_35;
+x_35 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__11;
+x_36 = lean_alloc_ctor(10, 2, 0);
+lean_ctor_set(x_36, 0, x_34);
+lean_ctor_set(x_36, 1, x_35);
+x_37 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__3;
+x_38 = lean_alloc_ctor(11, 2, 0);
+lean_ctor_set(x_38, 0, x_37);
+lean_ctor_set(x_38, 1, x_36);
+x_39 = l_Lean_logWarning___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__2(x_38, x_2, x_3, x_4, x_5, x_6, x_7, x_12);
+return x_39;
 }
 }
 }
 else
 {
-lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; 
-x_36 = lean_ctor_get(x_9, 0);
-x_37 = lean_ctor_get(x_9, 1);
-lean_inc(x_37);
-lean_inc(x_36);
+lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; 
+x_40 = lean_ctor_get(x_9, 0);
+x_41 = lean_ctor_get(x_9, 1);
+lean_inc(x_41);
+lean_inc(x_40);
 lean_dec(x_9);
-x_38 = lean_ctor_get(x_36, 0);
-lean_inc(x_38);
-lean_dec(x_36);
-x_39 = lean_box(0);
-x_40 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__1;
+x_42 = lean_ctor_get(x_40, 0);
+lean_inc(x_42);
+lean_dec(x_40);
+x_43 = lean_box(0);
+x_44 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__1;
 lean_inc(x_1);
-x_41 = l_Lean_ParametricAttribute_getParam_x3f___rarg(x_39, x_40, x_38, x_1);
-if (lean_obj_tag(x_41) == 0)
+x_45 = l_Lean_ParametricAttribute_getParam_x3f___rarg(x_43, x_44, x_42, x_1);
+if (lean_obj_tag(x_45) == 0)
 {
-lean_object* x_42; lean_object* x_43; 
+lean_object* x_46; lean_object* x_47; 
 lean_dec(x_7);
 lean_dec(x_6);
 lean_dec(x_5);
@ -57234,61 +57262,69 @@ lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_42 = lean_box(0);
-x_43 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_43, 0, x_42);
-lean_ctor_set(x_43, 1, x_37);
-return x_43;
-}
-else
-{
-lean_object* x_44; 
-x_44 = lean_ctor_get(x_41, 0);
-lean_inc(x_44);
-lean_dec(x_41);
-if (lean_obj_tag(x_44) == 0)
-{
-lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; 
-x_45 = lean_alloc_ctor(4, 1, 0);
-lean_ctor_set(x_45, 0, x_1);
-x_46 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__3;
-x_47 = lean_alloc_ctor(10, 2, 0);
+x_46 = lean_box(0);
+x_47 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_47, 0, x_46);
-lean_ctor_set(x_47, 1, x_45);
-x_48 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__5;
-x_49 = lean_alloc_ctor(10, 2, 0);
-lean_ctor_set(x_49, 0, x_47);
-lean_ctor_set(x_49, 1, x_48);
-x_50 = l_Lean_logWarning___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__2(x_49, x_2, x_3, x_4, x_5, x_6, x_7, x_37);
-return x_50;
+lean_ctor_set(x_47, 1, x_41);
+return x_47;
 }
 else
 {
-lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; 
-x_51 = lean_ctor_get(x_44, 0);
-lean_inc(x_51);
-lean_dec(x_44);
-x_52 = lean_alloc_ctor(4, 1, 0);
-lean_ctor_set(x_52, 0, x_1);
-x_53 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__3;
-x_54 = lean_alloc_ctor(10, 2, 0);
-lean_ctor_set(x_54, 0, x_53);
-lean_ctor_set(x_54, 1, x_52);
-x_55 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__7;
-x_56 = lean_alloc_ctor(10, 2, 0);
-lean_ctor_set(x_56, 0, x_54);
-lean_ctor_set(x_56, 1, x_55);
-x_57 = lean_alloc_ctor(4, 1, 0);
-lean_ctor_set(x_57, 0, x_51);
-x_58 = lean_alloc_ctor(10, 2, 0);
-lean_ctor_set(x_58, 0, x_56);
-lean_ctor_set(x_58, 1, x_57);
-x_59 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__9;
+lean_object* x_48; 
+x_48 = lean_ctor_get(x_45, 0);
+lean_inc(x_48);
+lean_dec(x_45);
+if (lean_obj_tag(x_48) == 0)
+{
+lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; 
+x_49 = lean_alloc_ctor(4, 1, 0);
+lean_ctor_set(x_49, 0, x_1);
+x_50 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__5;
+x_51 = lean_alloc_ctor(10, 2, 0);
+lean_ctor_set(x_51, 0, x_50);
+lean_ctor_set(x_51, 1, x_49);
+x_52 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__7;
+x_53 = lean_alloc_ctor(10, 2, 0);
+lean_ctor_set(x_53, 0, x_51);
+lean_ctor_set(x_53, 1, x_52);
+x_54 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__3;
+x_55 = lean_alloc_ctor(11, 2, 0);
+lean_ctor_set(x_55, 0, x_54);
+lean_ctor_set(x_55, 1, x_53);
+x_56 = l_Lean_logWarning___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__2(x_55, x_2, x_3, x_4, x_5, x_6, x_7, x_41);
+return x_56;
+}
+else
+{
+lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; 
+x_57 = lean_ctor_get(x_48, 0);
+lean_inc(x_57);
+lean_dec(x_48);
+x_58 = lean_alloc_ctor(4, 1, 0);
+lean_ctor_set(x_58, 0, x_1);
+x_59 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__5;
 x_60 = lean_alloc_ctor(10, 2, 0);
-lean_ctor_set(x_60, 0, x_58);
-lean_ctor_set(x_60, 1, x_59);
-x_61 = l_Lean_logWarning___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__2(x_60, x_2, x_3, x_4, x_5, x_6, x_7, x_37);
-return x_61;
+lean_ctor_set(x_60, 0, x_59);
+lean_ctor_set(x_60, 1, x_58);
+x_61 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__9;
+x_62 = lean_alloc_ctor(10, 2, 0);
+lean_ctor_set(x_62, 0, x_60);
+lean_ctor_set(x_62, 1, x_61);
+x_63 = lean_alloc_ctor(4, 1, 0);
+lean_ctor_set(x_63, 0, x_57);
+x_64 = lean_alloc_ctor(10, 2, 0);
+lean_ctor_set(x_64, 0, x_62);
+lean_ctor_set(x_64, 1, x_63);
+x_65 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__11;
+x_66 = lean_alloc_ctor(10, 2, 0);
+lean_ctor_set(x_66, 0, x_64);
+lean_ctor_set(x_66, 1, x_65);
+x_67 = l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__3;
+x_68 = lean_alloc_ctor(11, 2, 0);
+lean_ctor_set(x_68, 0, x_67);
+lean_ctor_set(x_68, 1, x_66);
+x_69 = l_Lean_logWarning___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__2(x_68, x_2, x_3, x_4, x_5, x_6, x_7, x_41);
+return x_69;
 }
 }
 }
@ -65886,6 +65922,10 @@ l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts_
 lean_mark_persistent(l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__8);
 l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__9 = _init_l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__9();
 lean_mark_persistent(l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__9);
+l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__10 = _init_l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__10();
+lean_mark_persistent(l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__10);
+l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__11 = _init_l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__11();
+lean_mark_persistent(l_Lean_checkDeprecated___at___private_Lean_Elab_Term_0__Lean_Elab_Term_mkConsts___spec__1___closed__11);
 l_Lean_Elab_throwAutoBoundImplicitLocal___at_Lean_Elab_Term_resolveName_process___spec__1___closed__1 = _init_l_Lean_Elab_throwAutoBoundImplicitLocal___at_Lean_Elab_Term_resolveName_process___spec__1___closed__1();
 lean_mark_persistent(l_Lean_Elab_throwAutoBoundImplicitLocal___at_Lean_Elab_Term_resolveName_process___spec__1___closed__1);
 l_Lean_Elab_throwAutoBoundImplicitLocal___at_Lean_Elab_Term_resolveName_process___spec__1___closed__2 = _init_l_Lean_Elab_throwAutoBoundImplicitLocal___at_Lean_Elab_Term_resolveName_process___spec__1___closed__2();
--- a/stage0/stdlib/Lean/Linter/Builtin.c
+++ b/stage0/stdlib/Lean/Linter/Builtin.c
@ -87,6 +87,7 @@ static lean_object* l_Lean_Linter_suspiciousUnexpanderPatterns___lambda__5___clo
 lean_object* l_Array_sequenceMap___at___aux__Init__NotationExtra______macroRules__term_x25_x5b___x7c___x5d__1___spec__1(lean_object*, lean_object*);
 static lean_object* l_Lean_Linter_suspiciousUnexpanderPatterns___lambda__4___closed__7;
 LEAN_EXPORT lean_object* l_Lean_Linter_suspiciousUnexpanderPatterns___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___lambda__1___closed__4;
 uint8_t l_Lean_Syntax_isNone(lean_object*);
 static lean_object* l_Lean_Linter_suspiciousUnexpanderPatterns___lambda__5___closed__2;
 static lean_object* l_Array_anyMUnsafe_any___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__4___closed__2;
@ -102,6 +103,7 @@ static lean_object* l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpand
 static lean_object* l_Lean_Linter_suspiciousUnexpanderPatterns___lambda__4___closed__5;
 static lean_object* l_Lean_Linter_suspiciousUnexpanderPatterns___lambda__5___closed__6;
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_Builtin___hyg_6____closed__2;
+static lean_object* l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___lambda__1___closed__3;
 static lean_object* l_Lean_Linter_suspiciousUnexpanderPatterns___lambda__4___closed__10;
 uint8_t l_Lean_Syntax_matchesIdent(lean_object*, lean_object*);
 static lean_object* l_Lean_Linter_suspiciousUnexpanderPatterns___lambda__5___closed__3;
@ -313,6 +315,26 @@ x_1 = lean_mk_string_from_bytes("Unexpanders should match the function name agai
 return x_1;
 }
 }
+static lean_object* _init_l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___lambda__1___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___lambda__1___closed__2;
+x_2 = lean_alloc_ctor(2, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___lambda__1___closed__4() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___lambda__1___closed__3;
+x_2 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
@ -335,7 +357,7 @@ lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; uint8_t x_
 x_9 = lean_ctor_get(x_6, 0);
 lean_inc(x_9);
 lean_dec(x_6);
-x_10 = l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___lambda__1___closed__2;
+x_10 = l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___lambda__1___closed__4;
 x_11 = 1;
 x_12 = l_Lean_Linter_publishMessage(x_10, x_9, x_11, x_2, x_3, x_4);
 lean_dec(x_9);
@ -2114,6 +2136,10 @@ l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3
 lean_mark_persistent(l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___lambda__1___closed__1);
 l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___lambda__1___closed__2 = _init_l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___lambda__1___closed__2();
 lean_mark_persistent(l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___lambda__1___closed__2);
+l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___lambda__1___closed__3 = _init_l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___lambda__1___closed__3();
+lean_mark_persistent(l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___lambda__1___closed__3);
+l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___lambda__1___closed__4 = _init_l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___lambda__1___closed__4();
+lean_mark_persistent(l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___lambda__1___closed__4);
 l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___closed__1 = _init_l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___closed__1();
 lean_mark_persistent(l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___closed__1);
 l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___closed__2 = _init_l_Array_forInUnsafe_loop___at_Lean_Linter_suspiciousUnexpanderPatterns___spec__3___closed__2();
--- a/stage0/stdlib/Lean/Linter/MissingDocs.c
+++ b/stage0/stdlib/Lean/Linter/MissingDocs.c
--- a/stage0/stdlib/Lean/Linter/UnusedVariables.c
+++ b/stage0/stdlib/Lean/Linter/UnusedVariables.c
@ -109,7 +109,6 @@ lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
 lean_object* l_Lean_Elab_Info_updateContext_x3f(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Linter_getLinterUnusedVariablesFunArgs___boxed(lean_object*);
-lean_object* lean_string_append(lean_object*, lean_object*);
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_295____lambda__1___closed__13;
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_225____lambda__1___closed__8;
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_1896____closed__7;
@ -158,12 +157,14 @@ static lean_object* l_List_foldr___at_Lean_Linter_initFn____x40_Lean_Linter_Unus
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_125____closed__1;
 LEAN_EXPORT uint8_t l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_1628____lambda__1(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_1722____lambda__1___closed__7;
+uint8_t l_Lean_MessageData_hasTag(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_225____lambda__1___boxed(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_1896____closed__1;
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_225____lambda__1___closed__1;
 LEAN_EXPORT lean_object* l_List_foldl___at_Lean_Linter_unusedVariables___spec__6(lean_object*, lean_object*);
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_1481____lambda__1___closed__5;
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_201____closed__1;
+LEAN_EXPORT uint8_t l_Lean_MessageData_isUnusedVariableWarning___lambda__1(lean_object*);
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_7____closed__1;
 static lean_object* l_Lean_Linter_getUnusedVariablesIgnoreFnsImpl___closed__1;
 LEAN_EXPORT lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_1514____lambda__1___boxed(lean_object*, lean_object*, lean_object*);
@ -179,6 +180,8 @@ LEAN_EXPORT uint8_t l_Lean_Linter_getLinterUnusedVariablesFunArgs(lean_object*);
 LEAN_EXPORT lean_object* l_Std_mkHashMap___at_Lean_Linter_unusedVariables___spec__1___boxed(lean_object*);
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_467____lambda__1___closed__9;
 lean_object* lean_array_fget(lean_object*, lean_object*);
+static lean_object* l_Lean_MessageData_isUnusedVariableWarning___closed__1;
+LEAN_EXPORT lean_object* l_Lean_MessageData_isUnusedVariableWarning___boxed(lean_object*);
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 uint8_t l___private_Lean_Attributes_0__Lean_beqAttributeKind____x40_Lean_Attributes___hyg_192_(uint8_t, uint8_t);
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_1514____closed__1;
@ -188,6 +191,7 @@ uint8_t l_Lean_Syntax_matchesNull(lean_object*, lean_object*);
 LEAN_EXPORT uint8_t l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_201____lambda__1(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_1514____lambda__1___closed__5;
 uint8_t l_String_Range_contains(lean_object*, lean_object*, uint8_t);
+static lean_object* l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__4;
 lean_object* lean_st_ref_take(lean_object*, lean_object*);
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_1896____closed__2;
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_225____lambda__1___closed__13;
@ -235,6 +239,7 @@ lean_object* l_Std_HashSetImp_insert___at_Lean_MVarId_getNondepPropHyps___spec__
 lean_object* lean_st_mk_ref(lean_object*, lean_object*);
 static lean_object* l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__2;
 static lean_object* l_List_foldr___at_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_1778____spec__1___closed__4;
+static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_3765____closed__1;
 static lean_object* l_Array_anyMUnsafe_any___at_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_550____spec__3___closed__5;
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_550____lambda__5___closed__12;
 lean_object* l_Lean_Syntax_getId(lean_object*);
@ -243,7 +248,6 @@ LEAN_EXPORT lean_object* l_Lean_Linter_unusedVariablesIgnoreFnsExt;
 LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Linter_unusedVariables_skipDeclIdIfPresent___closed__2;
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_7____closed__5;
-static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_3760____closed__1;
 LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT uint8_t l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_550____lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_1514____lambda__1___closed__9;
@ -267,6 +271,7 @@ LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Linter_unusedVariables
 LEAN_EXPORT lean_object* l_List_foldr___at_Lean_Linter_unusedVariables___spec__28___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_replace___at_Lean_Linter_unusedVariables___spec__7___boxed(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Linter_getLinterUnusedVariables___closed__1;
+LEAN_EXPORT lean_object* l_Lean_MessageData_isUnusedVariableWarning___lambda__1___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Linter_collectMacroExpansions_x3f___at_Lean_Linter_unusedVariables___spec__21(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Linter_collectMacroExpansions_x3f_go___at_Lean_Linter_unusedVariables___spec__22___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Linter_getLinterUnusedVariables___boxed(lean_object*);
@ -292,6 +297,7 @@ lean_object* l_List_filterMap___at_Lean_Linter_collectMacroExpansions_x3f_go___s
 LEAN_EXPORT lean_object* l_panic___at_Lean_Linter_unusedVariables___spec__25(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_550____lambda__5___closed__7;
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_384____lambda__1___closed__1;
+static lean_object* l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__5;
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_384____lambda__1___closed__4;
 size_t lean_usize_of_nat(lean_object*);
 lean_object* l_Std_HashMap_insert___at_Lean_Meta_AbstractMVars_abstractExprMVars___spec__4(lean_object*, lean_object*, lean_object*);
@ -348,6 +354,7 @@ static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hy
 LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at_Lean_Linter_unusedVariables___spec__35___lambda__1(lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Linter_collectMacroExpansions_x3f_go___at_Lean_Linter_unusedVariables___spec__22___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT uint8_t l_Lean_MessageData_isUnusedVariableWarning(lean_object*);
 LEAN_EXPORT uint8_t l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_260____lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentArray_toArray___rarg(lean_object*);
 lean_object* l_List_filterMap___at_Lean_Linter_collectMacroExpansions_x3f_go___spec__2(lean_object*);
@ -417,7 +424,7 @@ static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hy
 uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_1722____lambda__1___closed__9;
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_1854____closed__5;
-LEAN_EXPORT lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_3760_(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_3765_(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_225_(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_260_(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_39_(lean_object*);
@ -460,6 +467,7 @@ lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_HashSetImp_contains___at_Lean_Linter_unusedVariables_isTopLevelDecl___spec__1___boxed(lean_object*, lean_object*);
 static lean_object* l_List_foldr___at_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_1778____spec__1___closed__1;
 static lean_object* l_Array_anyMUnsafe_any___at_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_550____spec__3___closed__4;
+static lean_object* l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__6;
 LEAN_EXPORT lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_1854____lambda__2(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_1722____lambda__1___boxed(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_1481____lambda__1___closed__9;
@ -7836,7 +7844,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l_Lean_Elab_InfoTree_visitM_go___at_Lean_Linter_unusedVariables___spec__24___closed__1;
 x_2 = l_Lean_Elab_InfoTree_visitM_go___at_Lean_Linter_unusedVariables___spec__24___closed__2;
-x_3 = lean_unsigned_to_nat(39u);
+x_3 = lean_unsigned_to_nat(36u);
 x_4 = lean_unsigned_to_nat(21u);
 x_5 = l_Lean_Elab_InfoTree_visitM_go___at_Lean_Linter_unusedVariables___spec__24___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -8977,12 +8985,31 @@ return x_16;
 static lean_object* _init_l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__1() {
 _start:
 {
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_1896____closed__2;
+x_2 = l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_7____closed__3;
+x_3 = l_Lean_Name_str___override(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__2() {
+_start:
+{
 lean_object* x_1; 
 x_1 = lean_mk_string_from_bytes("unused variable `", 17);
 return x_1;
 }
 }
-static lean_object* _init_l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__2() {
+static lean_object* _init_l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__3() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__2;
+x_2 = l_Lean_stringToMessageData(x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__4() {
 _start:
 {
 lean_object* x_1; 
@ -8990,7 +9017,16 @@ x_1 = lean_mk_string_from_bytes("` [linter.unusedVariables]", 26);
 return x_1;
 }
 }
-static lean_object* _init_l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__3() {
+static lean_object* _init_l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__5() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__4;
+x_2 = l_Lean_stringToMessageData(x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
@ -9003,38 +9039,45 @@ return x_2;
 LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
 _start:
 {
-lean_object* x_7; uint8_t x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14; lean_object* x_15; uint8_t x_16; 
+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_object* x_13; lean_object* x_14; uint8_t x_15; lean_object* x_16; uint8_t x_17; 
 x_7 = l_Lean_LocalDecl_userName(x_1);
-x_8 = 1;
-x_9 = l_Lean_Name_toString(x_7, x_8);
-x_10 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__1;
-x_11 = lean_string_append(x_10, x_9);
-lean_dec(x_9);
-x_12 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__2;
-x_13 = lean_string_append(x_11, x_12);
-x_14 = 1;
-x_15 = l_Lean_Linter_publishMessage(x_13, x_2, x_14, x_4, x_5, x_6);
-x_16 = !lean_is_exclusive(x_15);
-if (x_16 == 0)
+x_8 = lean_alloc_ctor(4, 1, 0);
+lean_ctor_set(x_8, 0, x_7);
+x_9 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__3;
+x_10 = lean_alloc_ctor(10, 2, 0);
+lean_ctor_set(x_10, 0, x_9);
+lean_ctor_set(x_10, 1, x_8);
+x_11 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__5;
+x_12 = lean_alloc_ctor(10, 2, 0);
+lean_ctor_set(x_12, 0, x_10);
+lean_ctor_set(x_12, 1, x_11);
+x_13 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__1;
+x_14 = lean_alloc_ctor(11, 2, 0);
+lean_ctor_set(x_14, 0, x_13);
+lean_ctor_set(x_14, 1, x_12);
+x_15 = 1;
+x_16 = l_Lean_Linter_publishMessage(x_14, x_2, x_15, x_4, x_5, x_6);
+x_17 = !lean_is_exclusive(x_16);
+if (x_17 == 0)
 {
-lean_object* x_17; lean_object* x_18; 
-x_17 = lean_ctor_get(x_15, 0);
-lean_dec(x_17);
-x_18 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__3;
-lean_ctor_set(x_15, 0, x_18);
-return x_15;
+lean_object* x_18; lean_object* x_19; 
+x_18 = lean_ctor_get(x_16, 0);
+lean_dec(x_18);
+x_19 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__6;
+lean_ctor_set(x_16, 0, x_19);
+return x_16;
 }
 else
 {
-lean_object* x_19; lean_object* x_20; lean_object* x_21; 
-x_19 = lean_ctor_get(x_15, 1);
-lean_inc(x_19);
-lean_dec(x_15);
-x_20 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__3;
-x_21 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_21, 0, x_20);
-lean_ctor_set(x_21, 1, x_19);
-return x_21;
+lean_object* x_20; lean_object* x_21; lean_object* x_22; 
+x_20 = lean_ctor_get(x_16, 1);
+lean_inc(x_20);
+lean_dec(x_16);
+x_21 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__6;
+x_22 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_22, 0, x_21);
+lean_ctor_set(x_22, 1, x_20);
+return x_22;
 }
 }
 }
@ -9137,7 +9180,7 @@ lean_object* x_18; lean_object* x_19;
 lean_dec(x_12);
 lean_dec(x_11);
 lean_dec(x_2);
-x_18 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__3;
+x_18 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__6;
 x_19 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_19, 0, x_18);
 lean_ctor_set(x_19, 1, x_15);
@ -9163,7 +9206,7 @@ lean_dec(x_7);
 lean_dec(x_6);
 lean_dec(x_5);
 lean_dec(x_2);
-x_16 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__3;
+x_16 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__6;
 x_17 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_17, 0, x_16);
 lean_ctor_set(x_17, 1, x_14);
@ -9226,7 +9269,7 @@ lean_dec(x_7);
 lean_dec(x_6);
 lean_dec(x_5);
 lean_dec(x_2);
-x_32 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__3;
+x_32 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__6;
 x_33 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_33, 0, x_32);
 lean_ctor_set(x_33, 1, x_14);
@ -9262,7 +9305,7 @@ lean_dec(x_7);
 lean_dec(x_6);
 lean_dec(x_3);
 lean_dec(x_2);
-x_19 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__3;
+x_19 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__6;
 x_20 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_20, 0, x_19);
 lean_ctor_set(x_20, 1, x_14);
@ -9299,7 +9342,7 @@ lean_dec(x_6);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_19 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__3;
+x_19 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__6;
 x_20 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_20, 0, x_19);
 lean_ctor_set(x_20, 1, x_17);
@ -9369,7 +9412,7 @@ lean_dec(x_6);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_36 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__3;
+x_36 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__6;
 x_37 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_37, 0, x_36);
 lean_ctor_set(x_37, 1, x_17);
@ -9391,7 +9434,7 @@ lean_dec(x_6);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_38 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__3;
+x_38 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__6;
 x_39 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_39, 0, x_38);
 lean_ctor_set(x_39, 1, x_17);
@ -10972,7 +11015,7 @@ lean_dec(x_5);
 return x_12;
 }
 }
-static lean_object* _init_l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_3760____closed__1() {
+static lean_object* _init_l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_3765____closed__1() {
 _start:
 {
 lean_object* x_1; 
@ -10980,15 +11023,60 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Linter_unusedVariables), 4, 0);
 return x_1;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_3760_(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_3765_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
-x_2 = l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_3760____closed__1;
+x_2 = l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_3765____closed__1;
 x_3 = l_Lean_Elab_Command_addLinter(x_2, x_1);
 return x_3;
 }
 }
+LEAN_EXPORT uint8_t l_Lean_MessageData_isUnusedVariableWarning___lambda__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; uint8_t x_3; 
+x_2 = l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__1;
+x_3 = lean_name_eq(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l_Lean_MessageData_isUnusedVariableWarning___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_MessageData_isUnusedVariableWarning___lambda__1___boxed), 1, 0);
+return x_1;
+}
+}
+LEAN_EXPORT uint8_t l_Lean_MessageData_isUnusedVariableWarning(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; uint8_t x_3; 
+x_2 = l_Lean_MessageData_isUnusedVariableWarning___closed__1;
+x_3 = l_Lean_MessageData_hasTag(x_2, x_1);
+return x_3;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_MessageData_isUnusedVariableWarning___lambda__1___boxed(lean_object* x_1) {
+_start:
+{
+uint8_t x_2; lean_object* x_3; 
+x_2 = l_Lean_MessageData_isUnusedVariableWarning___lambda__1(x_1);
+lean_dec(x_1);
+x_3 = lean_box(x_2);
+return x_3;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_MessageData_isUnusedVariableWarning___boxed(lean_object* x_1) {
+_start:
+{
+uint8_t x_2; lean_object* x_3; 
+x_2 = l_Lean_MessageData_isUnusedVariableWarning(x_1);
+x_3 = lean_box(x_2);
+return x_3;
+}
+}
 lean_object* initialize_Init(uint8_t builtin, lean_object*);
 lean_object* initialize_Lean_Elab_Command(uint8_t builtin, lean_object*);
 lean_object* initialize_Lean_Linter_Util(uint8_t builtin, lean_object*);
@ -11484,6 +11572,12 @@ l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___clos
 lean_mark_persistent(l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__2);
 l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__3 = _init_l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__3();
 lean_mark_persistent(l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__3);
+l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__4 = _init_l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__4();
+lean_mark_persistent(l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__4);
+l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__5 = _init_l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__5();
+lean_mark_persistent(l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__5);
+l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__6 = _init_l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__6();
+lean_mark_persistent(l_List_forIn_loop___at_Lean_Linter_unusedVariables___spec__32___lambda__1___closed__6);
 l_Std_AssocList_foldlM___at_Lean_Linter_unusedVariables___spec__33___closed__1 = _init_l_Std_AssocList_foldlM___at_Lean_Linter_unusedVariables___spec__33___closed__1();
 lean_mark_persistent(l_Std_AssocList_foldlM___at_Lean_Linter_unusedVariables___spec__33___closed__1);
 l_Std_AssocList_foldlM___at_Lean_Linter_unusedVariables___spec__33___closed__2 = _init_l_Std_AssocList_foldlM___at_Lean_Linter_unusedVariables___spec__33___closed__2();
@ -11494,11 +11588,13 @@ l_Array_foldrMUnsafe_fold___at_Lean_Linter_unusedVariables___spec__35___closed__
 lean_mark_persistent(l_Array_foldrMUnsafe_fold___at_Lean_Linter_unusedVariables___spec__35___closed__1);
 l_Lean_Linter_unusedVariables___lambda__1___closed__1 = _init_l_Lean_Linter_unusedVariables___lambda__1___closed__1();
 lean_mark_persistent(l_Lean_Linter_unusedVariables___lambda__1___closed__1);
-l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_3760____closed__1 = _init_l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_3760____closed__1();
-lean_mark_persistent(l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_3760____closed__1);
-res = l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_3760_(lean_io_mk_world());
+l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_3765____closed__1 = _init_l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_3765____closed__1();
+lean_mark_persistent(l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_3765____closed__1);
+res = l_Lean_Linter_initFn____x40_Lean_Linter_UnusedVariables___hyg_3765_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+l_Lean_MessageData_isUnusedVariableWarning___closed__1 = _init_l_Lean_MessageData_isUnusedVariableWarning___closed__1();
+lean_mark_persistent(l_Lean_MessageData_isUnusedVariableWarning___closed__1);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus
--- a/stage0/stdlib/Lean/Linter/Util.c
+++ b/stage0/stdlib/Lean/Linter/Util.c
@ -260,7 +260,7 @@ return x_4;
 LEAN_EXPORT lean_object* l_Lean_Linter_publishMessage(lean_object* x_1, lean_object* x_2, uint8_t x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
 _start:
 {
-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_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22; 
+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_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; uint8_t x_20; 
 x_7 = lean_st_ref_get(x_5, x_6);
 x_8 = lean_ctor_get(x_7, 0);
 lean_inc(x_8);
@ -272,105 +272,101 @@ lean_inc(x_10);
 x_11 = lean_ctor_get(x_4, 1);
 lean_inc(x_11);
 lean_dec(x_4);
-x_12 = lean_alloc_ctor(2, 1, 0);
-lean_ctor_set(x_12, 0, x_1);
-x_13 = lean_alloc_ctor(0, 1, 0);
-lean_ctor_set(x_13, 0, x_12);
-x_14 = lean_ctor_get(x_2, 0);
-x_15 = lean_ctor_get(x_2, 1);
-x_16 = l_Lean_Elab_mkMessageCore(x_10, x_11, x_13, x_3, x_14, x_15);
+x_12 = lean_ctor_get(x_2, 0);
+x_13 = lean_ctor_get(x_2, 1);
+x_14 = l_Lean_Elab_mkMessageCore(x_10, x_11, x_1, x_3, x_12, x_13);
 lean_dec(x_11);
-x_17 = lean_ctor_get(x_8, 1);
-lean_inc(x_17);
+x_15 = lean_ctor_get(x_8, 1);
+lean_inc(x_15);
 lean_dec(x_8);
-x_18 = l_Std_PersistentArray_push___rarg(x_17, x_16);
-x_19 = lean_st_ref_take(x_5, x_9);
-x_20 = lean_ctor_get(x_19, 0);
-lean_inc(x_20);
-x_21 = lean_ctor_get(x_19, 1);
-lean_inc(x_21);
-lean_dec(x_19);
-x_22 = !lean_is_exclusive(x_20);
-if (x_22 == 0)
+x_16 = l_Std_PersistentArray_push___rarg(x_15, x_14);
+x_17 = lean_st_ref_take(x_5, x_9);
+x_18 = lean_ctor_get(x_17, 0);
+lean_inc(x_18);
+x_19 = lean_ctor_get(x_17, 1);
+lean_inc(x_19);
+lean_dec(x_17);
+x_20 = !lean_is_exclusive(x_18);
+if (x_20 == 0)
 {
-lean_object* x_23; lean_object* x_24; uint8_t x_25; 
-x_23 = lean_ctor_get(x_20, 1);
-lean_dec(x_23);
-lean_ctor_set(x_20, 1, x_18);
-x_24 = lean_st_ref_set(x_5, x_20, x_21);
-x_25 = !lean_is_exclusive(x_24);
-if (x_25 == 0)
+lean_object* x_21; lean_object* x_22; uint8_t x_23; 
+x_21 = lean_ctor_get(x_18, 1);
+lean_dec(x_21);
+lean_ctor_set(x_18, 1, x_16);
+x_22 = lean_st_ref_set(x_5, x_18, x_19);
+x_23 = !lean_is_exclusive(x_22);
+if (x_23 == 0)
 {
-lean_object* x_26; lean_object* x_27; 
-x_26 = lean_ctor_get(x_24, 0);
-lean_dec(x_26);
-x_27 = lean_box(0);
-lean_ctor_set(x_24, 0, x_27);
-return x_24;
-}
-else
-{
-lean_object* x_28; lean_object* x_29; lean_object* x_30; 
-x_28 = lean_ctor_get(x_24, 1);
-lean_inc(x_28);
+lean_object* x_24; lean_object* x_25; 
+x_24 = lean_ctor_get(x_22, 0);
 lean_dec(x_24);
-x_29 = lean_box(0);
-x_30 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_30, 0, x_29);
-lean_ctor_set(x_30, 1, x_28);
-return x_30;
+x_25 = lean_box(0);
+lean_ctor_set(x_22, 0, x_25);
+return x_22;
+}
+else
+{
+lean_object* x_26; lean_object* x_27; lean_object* x_28; 
+x_26 = lean_ctor_get(x_22, 1);
+lean_inc(x_26);
+lean_dec(x_22);
+x_27 = lean_box(0);
+x_28 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_28, 0, x_27);
+lean_ctor_set(x_28, 1, x_26);
+return x_28;
 }
 }
 else
 {
-lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; 
-x_31 = lean_ctor_get(x_20, 0);
-x_32 = lean_ctor_get(x_20, 2);
-x_33 = lean_ctor_get(x_20, 3);
-x_34 = lean_ctor_get(x_20, 4);
-x_35 = lean_ctor_get(x_20, 5);
-x_36 = lean_ctor_get(x_20, 6);
-x_37 = lean_ctor_get(x_20, 7);
-x_38 = lean_ctor_get(x_20, 8);
-lean_inc(x_38);
-lean_inc(x_37);
+lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; 
+x_29 = lean_ctor_get(x_18, 0);
+x_30 = lean_ctor_get(x_18, 2);
+x_31 = lean_ctor_get(x_18, 3);
+x_32 = lean_ctor_get(x_18, 4);
+x_33 = lean_ctor_get(x_18, 5);
+x_34 = lean_ctor_get(x_18, 6);
+x_35 = lean_ctor_get(x_18, 7);
+x_36 = lean_ctor_get(x_18, 8);
 lean_inc(x_36);
 lean_inc(x_35);
 lean_inc(x_34);
 lean_inc(x_33);
 lean_inc(x_32);
 lean_inc(x_31);
-lean_dec(x_20);
-x_39 = lean_alloc_ctor(0, 9, 0);
-lean_ctor_set(x_39, 0, x_31);
-lean_ctor_set(x_39, 1, x_18);
-lean_ctor_set(x_39, 2, x_32);
-lean_ctor_set(x_39, 3, x_33);
-lean_ctor_set(x_39, 4, x_34);
-lean_ctor_set(x_39, 5, x_35);
-lean_ctor_set(x_39, 6, x_36);
-lean_ctor_set(x_39, 7, x_37);
-lean_ctor_set(x_39, 8, x_38);
-x_40 = lean_st_ref_set(x_5, x_39, x_21);
-x_41 = lean_ctor_get(x_40, 1);
-lean_inc(x_41);
-if (lean_is_exclusive(x_40)) {
- lean_ctor_release(x_40, 0);
- lean_ctor_release(x_40, 1);
+lean_inc(x_30);
+lean_inc(x_29);
+lean_dec(x_18);
+x_37 = lean_alloc_ctor(0, 9, 0);
+lean_ctor_set(x_37, 0, x_29);
+lean_ctor_set(x_37, 1, x_16);
+lean_ctor_set(x_37, 2, x_30);
+lean_ctor_set(x_37, 3, x_31);
+lean_ctor_set(x_37, 4, x_32);
+lean_ctor_set(x_37, 5, x_33);
+lean_ctor_set(x_37, 6, x_34);
+lean_ctor_set(x_37, 7, x_35);
+lean_ctor_set(x_37, 8, x_36);
+x_38 = lean_st_ref_set(x_5, x_37, x_19);
+x_39 = lean_ctor_get(x_38, 1);
+lean_inc(x_39);
+if (lean_is_exclusive(x_38)) {
+ lean_ctor_release(x_38, 0);
+ lean_ctor_release(x_38, 1);
+ x_40 = x_38;
+} else {
+ lean_dec_ref(x_38);
+ x_40 = lean_box(0);
+}
+x_41 = lean_box(0);
+if (lean_is_scalar(x_40)) {
+ x_42 = lean_alloc_ctor(0, 2, 0);
+} else {
 x_42 = x_40;
-} else {
- lean_dec_ref(x_40);
- x_42 = lean_box(0);
 }
-x_43 = lean_box(0);
-if (lean_is_scalar(x_42)) {
- x_44 = lean_alloc_ctor(0, 2, 0);
-} else {
- x_44 = x_42;
-}
-lean_ctor_set(x_44, 0, x_43);
-lean_ctor_set(x_44, 1, x_41);
-return x_44;
+lean_ctor_set(x_42, 0, x_41);
+lean_ctor_set(x_42, 1, x_39);
+return x_42;
 }
 }
 }
--- a/stage0/stdlib/Lean/Meta/Tactic/Intro.c
+++ b/stage0/stdlib/Lean/Meta/Tactic/Intro.c
@ -44,6 +44,7 @@ lean_object* l_Lean_MVarId_withContext___at___private_Lean_Meta_SynthInstance_0_
 static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Intro___hyg_834____closed__3;
 static lean_object* l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_introNImp_loop___rarg___lambda__2___closed__16;
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_introNImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Meta_mkFreshBinderNameForTactic(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_usize_dec_lt(size_t, size_t);
 lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
@ -55,6 +56,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Intro___hyg_
 static lean_object* l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_introNImp_loop___rarg___lambda__2___closed__10;
 LEAN_EXPORT lean_object* l_Lean_Meta_intro(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_ReaderT_instMonadLiftReaderT(lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_mkFreshBinderNameForTacticCore(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Core_instMonadOptionsCoreM___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_ReaderT_instMonadLiftReaderT___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withNewLocalInstances___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -77,6 +79,8 @@ lean_object* l_Lean_monadNameGeneratorLift___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_instantiateMVars___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_cleanupAnnotations(lean_object*);
 lean_object* l_Lean_Expr_headBeta(lean_object*);
+static lean_object* l_Lean_Meta_mkFreshBinderNameForTactic___closed__1;
+LEAN_EXPORT lean_object* l_Lean_Meta_mkFreshBinderNameForTactic___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_introNImp_loop___rarg___lambda__1___closed__2;
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_introNImp_loop(lean_object*);
 lean_object* l_Lean_Meta_mkLambdaFVars(lean_object*, lean_object*, uint8_t, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -143,12 +147,12 @@ lean_object* l_Lean_instantiateMVars___at___private_Lean_Meta_Basic_0__Lean_Meta
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_getIntrosSize___boxed(lean_object*);
 static lean_object* l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_introNImp_loop___rarg___lambda__2___closed__8;
 LEAN_EXPORT lean_object* l_Lean_Meta_intro1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-static lean_object* l_Lean_Meta_introNCore___closed__1;
 static lean_object* l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_introNImp_loop___rarg___lambda__2___closed__3;
 LEAN_EXPORT lean_object* l_Lean_Meta_introNCore___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_ReaderT_instMonadReaderT___rarg(lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_introNImp_loop___rarg(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*);
 lean_object* l_Lean_Meta_mkFreshExprSyntheticOpaqueMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_mkFreshBinderNameForTacticCore___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_introNImp_loop___rarg___closed__2;
 lean_object* l_panic___at_Lean_Expr_fvarId_x21___spec__1(lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_introNImp_loop___rarg___lambda__1(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*, lean_object*);
@ -1649,68 +1653,120 @@ x_4 = l_Lean_Option_register___at_Std_Format_initFn____x40_Lean_Data_Format___hy
 return x_4;
 }
 }
+LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_mkFreshBinderNameForTacticCore(lean_object* x_1, lean_object* x_2, uint8_t x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
+_start:
+{
+if (x_3 == 0)
+{
+lean_object* x_9; lean_object* x_10; 
+x_9 = lean_local_ctx_get_unused_name(x_1, x_2);
+x_10 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_10, 0, x_9);
+lean_ctor_set(x_10, 1, x_8);
+return x_10;
+}
+else
+{
+lean_object* x_11; 
+lean_dec(x_1);
+x_11 = l___private_Lean_CoreM_0__Lean_Core_mkFreshNameImp(x_2, x_6, x_7, x_8);
+return x_11;
+}
+}
+}
+LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_mkFreshBinderNameForTacticCore___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
+_start:
+{
+uint8_t x_9; lean_object* x_10; 
+x_9 = lean_unbox(x_3);
+lean_dec(x_3);
+x_10 = l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_mkFreshBinderNameForTacticCore(x_1, x_2, x_9, x_4, x_5, x_6, x_7, x_8);
+lean_dec(x_7);
+lean_dec(x_6);
+lean_dec(x_5);
+lean_dec(x_4);
+return x_10;
+}
+}
+static lean_object* _init_l_Lean_Meta_mkFreshBinderNameForTactic___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Lean_Meta_tactic_hygienic;
+return x_1;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Meta_mkFreshBinderNameForTactic(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11; 
+x_7 = lean_ctor_get(x_2, 1);
+lean_inc(x_7);
+x_8 = lean_ctor_get(x_4, 2);
+x_9 = l_Lean_Meta_mkFreshBinderNameForTactic___closed__1;
+x_10 = l_Lean_Option_get___at_Lean_getSanitizeNames___spec__1(x_8, x_9);
+x_11 = l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_mkFreshBinderNameForTacticCore(x_7, x_1, x_10, x_2, x_3, x_4, x_5, x_6);
+lean_dec(x_2);
+return x_11;
+}
+}
+LEAN_EXPORT lean_object* l_Lean_Meta_mkFreshBinderNameForTactic___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+lean_object* x_7; 
+x_7 = l_Lean_Meta_mkFreshBinderNameForTactic(x_1, x_2, x_3, x_4, x_5, x_6);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+return x_7;
+}
+}
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_mkAuxNameImp_mkAuxNameWithoutGivenName(uint8_t x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
 _start:
 {
 if (x_1 == 0)
 {
-if (x_2 == 0)
+lean_object* x_11; uint8_t x_12; 
+x_11 = l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_mkFreshBinderNameForTacticCore(x_3, x_4, x_2, x_6, x_7, x_8, x_9, x_10);
+x_12 = !lean_is_exclusive(x_11);
+if (x_12 == 0)
 {
-lean_object* x_11; lean_object* x_12; lean_object* x_13; 
-x_11 = lean_local_ctx_get_unused_name(x_3, x_4);
-x_12 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_12, 0, x_11);
-lean_ctor_set(x_12, 1, x_5);
-x_13 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_13, 0, x_12);
-lean_ctor_set(x_13, 1, x_10);
-return x_13;
+lean_object* x_13; lean_object* x_14; 
+x_13 = lean_ctor_get(x_11, 0);
+x_14 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_14, 0, x_13);
+lean_ctor_set(x_14, 1, x_5);
+lean_ctor_set(x_11, 0, x_14);
+return x_11;
 }
 else
 {
-lean_object* x_14; uint8_t x_15; 
-lean_dec(x_3);
-x_14 = l___private_Lean_CoreM_0__Lean_Core_mkFreshNameImp(x_4, x_8, x_9, x_10);
-x_15 = !lean_is_exclusive(x_14);
-if (x_15 == 0)
-{
-lean_object* x_16; lean_object* x_17; 
-x_16 = lean_ctor_get(x_14, 0);
+lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; 
+x_15 = lean_ctor_get(x_11, 0);
+x_16 = lean_ctor_get(x_11, 1);
+lean_inc(x_16);
+lean_inc(x_15);
+lean_dec(x_11);
 x_17 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_17, 0, x_16);
+lean_ctor_set(x_17, 0, x_15);
 lean_ctor_set(x_17, 1, x_5);
-lean_ctor_set(x_14, 0, x_17);
-return x_14;
-}
-else
-{
-lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; 
-x_18 = lean_ctor_get(x_14, 0);
-x_19 = lean_ctor_get(x_14, 1);
-lean_inc(x_19);
-lean_inc(x_18);
-lean_dec(x_14);
-x_20 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_20, 0, x_18);
-lean_ctor_set(x_20, 1, x_5);
-x_21 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_21, 0, x_20);
-lean_ctor_set(x_21, 1, x_19);
-return x_21;
-}
+x_18 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_18, 0, x_17);
+lean_ctor_set(x_18, 1, x_16);
+return x_18;
 }
 }
 else
 {
-lean_object* x_22; lean_object* x_23; 
+lean_object* x_19; lean_object* x_20; 
 lean_dec(x_3);
-x_22 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_22, 0, x_4);
-lean_ctor_set(x_22, 1, x_5);
-x_23 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_23, 0, x_22);
-lean_ctor_set(x_23, 1, x_10);
-return x_23;
+x_19 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_19, 0, x_4);
+lean_ctor_set(x_19, 1, x_5);
+x_20 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_20, 0, x_19);
+lean_ctor_set(x_20, 1, x_10);
+return x_20;
 }
 }
 }
@ -1873,21 +1929,13 @@ lean_dec(x_8);
 return x_17;
 }
 }
-static lean_object* _init_l_Lean_Meta_introNCore___closed__1() {
-_start:
-{
-lean_object* x_1; 
-x_1 = l_Lean_Meta_tactic_hygienic;
-return x_1;
-}
-}
 LEAN_EXPORT lean_object* l_Lean_Meta_introNCore(lean_object* x_1, lean_object* x_2, lean_object* x_3, uint8_t x_4, uint8_t x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
 _start:
 {
 lean_object* x_11; lean_object* x_12; uint8_t x_13; lean_object* x_14; uint8_t x_15; 
 x_11 = lean_ctor_get(x_8, 2);
 lean_inc(x_11);
-x_12 = l_Lean_Meta_introNCore___closed__1;
+x_12 = l_Lean_Meta_mkFreshBinderNameForTactic___closed__1;
 x_13 = l_Lean_Option_get___at_Lean_getSanitizeNames___spec__1(x_11, x_12);
 lean_dec(x_11);
 x_14 = lean_unsigned_to_nat(0u);
@ -2681,12 +2729,12 @@ if (lean_io_result_is_error(res)) return res;
 l_Lean_Meta_tactic_hygienic = lean_io_result_get_value(res);
 lean_mark_persistent(l_Lean_Meta_tactic_hygienic);
 lean_dec_ref(res);
-}l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_mkAuxNameImp___closed__1 = _init_l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_mkAuxNameImp___closed__1();
+}l_Lean_Meta_mkFreshBinderNameForTactic___closed__1 = _init_l_Lean_Meta_mkFreshBinderNameForTactic___closed__1();
+lean_mark_persistent(l_Lean_Meta_mkFreshBinderNameForTactic___closed__1);
+l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_mkAuxNameImp___closed__1 = _init_l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_mkAuxNameImp___closed__1();
 lean_mark_persistent(l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_mkAuxNameImp___closed__1);
 l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_mkAuxNameImp___closed__2 = _init_l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_mkAuxNameImp___closed__2();
 lean_mark_persistent(l___private_Lean_Meta_Tactic_Intro_0__Lean_Meta_mkAuxNameImp___closed__2);
-l_Lean_Meta_introNCore___closed__1 = _init_l_Lean_Meta_introNCore___closed__1();
-lean_mark_persistent(l_Lean_Meta_introNCore___closed__1);
 l_Lean_MVarId_intro___closed__1 = _init_l_Lean_MVarId_intro___closed__1();
 lean_mark_persistent(l_Lean_MVarId_intro___closed__1);
 l_Lean_MVarId_intro___closed__2 = _init_l_Lean_MVarId_intro___closed__2();
--- a/stage0/stdlib/Lean/Server/InfoUtils.c
+++ b/stage0/stdlib/Lean/Server/InfoUtils.c
@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Lean.Server.InfoUtils
-// Imports: Init Lean.DocString Lean.Elab.InfoTree Lean.PrettyPrinter Lean.Util.Sorry
+// Imports: Init Lean.PrettyPrinter
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@ -1165,7 +1165,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l_Lean_Elab_InfoTree_visitM_go___rarg___closed__1;
 x_2 = l_Lean_Elab_InfoTree_visitM_go___rarg___closed__2;
-x_3 = lean_unsigned_to_nat(39u);
+x_3 = lean_unsigned_to_nat(36u);
 x_4 = lean_unsigned_to_nat(21u);
 x_5 = l_Lean_Elab_InfoTree_visitM_go___rarg___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -15259,10 +15259,7 @@ return x_4;
 }
 }
 lean_object* initialize_Init(uint8_t builtin, lean_object*);
-lean_object* initialize_Lean_DocString(uint8_t builtin, lean_object*);
-lean_object* initialize_Lean_Elab_InfoTree(uint8_t builtin, lean_object*);
 lean_object* initialize_Lean_PrettyPrinter(uint8_t builtin, lean_object*);
-lean_object* initialize_Lean_Util_Sorry(uint8_t builtin, lean_object*);
 static bool _G_initialized = false;
 LEAN_EXPORT lean_object* initialize_Lean_Server_InfoUtils(uint8_t builtin, lean_object* w) {
 lean_object * res;
@ -15271,18 +15268,9 @@ _G_initialized = true;
 res = initialize_Init(builtin, lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-res = initialize_Lean_DocString(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-res = initialize_Lean_Elab_InfoTree(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
 res = initialize_Lean_PrettyPrinter(builtin, lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-res = initialize_Lean_Util_Sorry(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
 l_String_instInhabitedRange___closed__1 = _init_l_String_instInhabitedRange___closed__1();
 lean_mark_persistent(l_String_instInhabitedRange___closed__1);
 l_String_instInhabitedRange = _init_l_String_instInhabitedRange();
--- a/stage0/stdlib/Lean/Server/References.c
+++ b/stage0/stdlib/Lean/Server/References.c
@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Lean.Server.References
-// Imports: Init Init.System.IO Lean.Data.Json Lean.Data.Lsp Lean.Server.Utils Lean.Server.InfoUtils Lean.Server.Snapshots
+// Imports: Init Lean.Server.Utils
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@ -3335,7 +3335,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l_Lean_Elab_InfoTree_visitM_go___at_Lean_Server_findReferences___spec__3___closed__1;
 x_2 = l_Lean_Elab_InfoTree_visitM_go___at_Lean_Server_findReferences___spec__3___closed__2;
-x_3 = lean_unsigned_to_nat(39u);
+x_3 = lean_unsigned_to_nat(36u);
 x_4 = lean_unsigned_to_nat(21u);
 x_5 = l_Lean_Elab_InfoTree_visitM_go___at_Lean_Server_findReferences___spec__3___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -12803,12 +12803,7 @@ return x_2;
 }
 }
 lean_object* initialize_Init(uint8_t builtin, lean_object*);
-lean_object* initialize_Init_System_IO(uint8_t builtin, lean_object*);
-lean_object* initialize_Lean_Data_Json(uint8_t builtin, lean_object*);
-lean_object* initialize_Lean_Data_Lsp(uint8_t builtin, lean_object*);
 lean_object* initialize_Lean_Server_Utils(uint8_t builtin, lean_object*);
-lean_object* initialize_Lean_Server_InfoUtils(uint8_t builtin, lean_object*);
-lean_object* initialize_Lean_Server_Snapshots(uint8_t builtin, lean_object*);
 static bool _G_initialized = false;
 LEAN_EXPORT lean_object* initialize_Lean_Server_References(uint8_t builtin, lean_object* w) {
 lean_object * res;
@ -12817,24 +12812,9 @@ _G_initialized = true;
 res = initialize_Init(builtin, lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-res = initialize_Init_System_IO(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-res = initialize_Lean_Data_Json(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-res = initialize_Lean_Data_Lsp(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
 res = initialize_Lean_Server_Utils(builtin, lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-res = initialize_Lean_Server_InfoUtils(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-res = initialize_Lean_Server_Snapshots(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
 l_Lean_Server_Reference_aliases___default___closed__1 = _init_l_Lean_Server_Reference_aliases___default___closed__1();
 lean_mark_persistent(l_Lean_Server_Reference_aliases___default___closed__1);
 l_Lean_Server_Reference_aliases___default = _init_l_Lean_Server_Reference_aliases___default();
--- a/stage0/stdlib/Lean/Widget/InteractiveDiagnostic.c
+++ b/stage0/stdlib/Lean/Widget/InteractiveDiagnostic.c
@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Lean.Widget.InteractiveDiagnostic
-// Imports: Init Lean.Data.Lsp Lean.Message Lean.Elab.InfoTree Lean.Server.Utils Lean.Server.Rpc.Basic Lean.Widget.Basic Lean.Widget.TaggedText Lean.Widget.InteractiveCode Lean.Widget.InteractiveGoal
+// Imports: Init Lean.Linter.UnusedVariables Lean.Server.Utils Lean.Widget.InteractiveGoal
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@ -18,7 +18,7 @@ LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingMsgE
 LEAN_EXPORT lean_object* l_Lean_Lsp_instRpcEncodingDiagnosticWith___rarg___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcDecode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__3___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcDecode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__16___rarg(lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Widget_msgToInteractiveDiagnostic___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Widget_msgToInteractiveDiagnostic___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Lsp_instRpcEncodingDiagnosticWith___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Lsp_instRpcEncodingDiagnosticWith___spec__20___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Lsp_instRpcEncodingDiagnosticWith___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -200,6 +200,7 @@ LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingMsgE
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcEncode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__4___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static uint32_t l_Lean_Widget_instInhabitedEmbedFmt___closed__7;
 lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Diagnostics_0__Lean_Lsp_fromJsonDiagnosticWith____x40_Lean_Data_Lsp_Diagnostics___hyg_1061____spec__3(lean_object*, lean_object*);
+uint8_t l_Lean_MessageData_hasTag(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcEncode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__26(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Widget_instRpcEncodingMsgEmbed_rpcEncode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____rarg___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Widget_InteractiveGoal_pretty(lean_object*);
@ -252,6 +253,7 @@ LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingMsgE
 LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcEncode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__24___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcEncode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__25___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_fromJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveDiagnostic___hyg_899____rarg___closed__1;
+static lean_object* l_Lean_Widget_msgToInteractiveDiagnostic___closed__10;
 LEAN_EXPORT lean_object* l_Lean_Widget_instRpcEncodingMsgEmbed_rpcDecode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcDecode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__16___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcEncode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__36___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -327,6 +329,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_instRpcEncoding
 LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcDecode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__15___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcDecode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__49(lean_object*);
 lean_object* lean_expr_dbg_to_string(lean_object*);
+lean_object* l_Lean_MessageData_isUnusedVariableWarning___lambda__1___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcEncode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__34(lean_object*);
 lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonRpcRef____x40_Lean_Data_Lsp_Extra___hyg_1095_(size_t);
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcDecode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__34___rarg___lambda__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -420,6 +423,7 @@ LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingMsgE
 static lean_object* l___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_fromJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveDiagnostic___hyg_899____rarg___closed__7;
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcDecode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__10___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcDecode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__50(lean_object*);
+static lean_object* l_Lean_Widget_msgToInteractiveDiagnostic___closed__9;
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcEncode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__26___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcDecode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__21(lean_object*);
 lean_object* l_Lean_JsonNumber_fromNat(lean_object*);
@ -430,6 +434,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_instRpcEncoding
 LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Lsp_instRpcEncodingDiagnosticWith___spec__16(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Lsp_instRpcEncodingDiagnosticWith___rarg___lambda__19(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcEncode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__11___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_Widget_msgToInteractiveDiagnostic___closed__8;
 lean_object* l___private_Lean_Widget_TaggedText_0__Lean_Widget_fromJsonTaggedText____x40_Lean_Widget_TaggedText___hyg_407____at___private_Lean_Widget_InteractiveGoal_0__Lean_Widget_fromJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveGoal___hyg_136____spec__6(lean_object*);
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcDecode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__10___rarg___lambda__1(size_t, lean_object*, lean_object*, size_t, lean_object*);
 LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcDecode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__8___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -472,6 +477,7 @@ LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Lsp_instRpcEncodingDiagnos
 LEAN_EXPORT lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcDecode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__38___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcDecode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__34___rarg___lambda__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcEncode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__7___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_Widget_msgToInteractiveDiagnostic___closed__6;
 LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Lsp_instRpcEncodingDiagnosticWith___spec__23___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcEncode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__27(lean_object*);
 LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcEncode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__6(lean_object*);
@ -501,6 +507,7 @@ LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingMsgE
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Lsp_instRpcEncodingDiagnosticWith___spec__5___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, size_t, uint8_t);
 LEAN_EXPORT lean_object* l_Lean_Widget_instRpcEncodingMsgEmbed_rpcEncode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____rarg___lambda__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcDecode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__31(lean_object*);
+static lean_object* l_Lean_Widget_msgToInteractiveDiagnostic___closed__11;
 LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Lsp_instRpcEncodingDiagnosticWith___spec__11___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Widget_InteractiveGoal_0__Lean_Widget_fromJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveGoal___hyg_718_(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Lsp_instRpcEncodingDiagnosticWith___rarg___lambda__9(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -565,6 +572,7 @@ LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingMsgE
 LEAN_EXPORT lean_object* l___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_msgToInteractiveAux___boxed(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_fromJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveDiagnostic___hyg_125____lambda__2(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Lsp_instRpcEncodingDiagnosticWith___spec__16___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_MessageData_isDeprecationWarning___lambda__1___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Widget_InteractiveDiagnostic_toDiagnostic_prettyTt___lambda__1___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcEncode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__26___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_StateT_pure___at___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_msgToInteractiveAux_go___spec__1___rarg(lean_object*, lean_object*, lean_object*);
@ -599,13 +607,13 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_instRpcEncoding
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcEncode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__34___rarg___boxed__const__1;
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcDecode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__34___rarg___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_formatStxAux(lean_object*, uint8_t, lean_object*, lean_object*);
-static lean_object* l_Lean_Widget_msgToInteractiveDiagnostic___lambda__1___closed__1;
 static lean_object* l___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_fromJsonRpcEncodingPacket____x40_Lean_Widget_InteractiveDiagnostic___hyg_125____lambda__2___closed__4;
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_msgToInteractive___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcDecode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__12(lean_object*);
 LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcDecode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__6(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Widget_instRpcEncodingMsgEmbed_rpcDecode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____rarg___lambda__2(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Lsp_instRpcEncodingDiagnosticWith___rarg___lambda__7(lean_object*, lean_object*);
+static lean_object* l_Lean_Widget_msgToInteractiveDiagnostic___closed__7;
 static lean_object* l_Lean_Widget_instInhabitedEmbedFmt___closed__1;
 LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcDecode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__19(lean_object*);
 lean_object* l_Lean_PrettyPrinter_ppExprWithInfos(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -620,7 +628,6 @@ uint8_t lean_string_dec_eq(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Lsp_instRpcEncodingDiagnosticWith___spec__2___rarg(lean_object*, lean_object*, size_t, size_t, lean_object*);
 lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Diagnostics_0__Lean_Lsp_fromJsonDiagnosticWith____x40_Lean_Data_Lsp_Diagnostics___hyg_1061____spec__2(lean_object*, lean_object*);
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
-static lean_object* l_Lean_Widget_msgToInteractiveDiagnostic___lambda__1___closed__2;
 LEAN_EXPORT lean_object* l_ExceptT_bindCont___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcEncode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__41(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Widget_InteractiveDiagnostic_toDiagnostic_prettyTt___lambda__1(lean_object*, lean_object*);
 static lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_instRpcEncodingMsgEmbed_rpcEncode____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____spec__34___rarg___lambda__8___closed__1;
@ -16745,7 +16752,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_1 = l_Lean_Widget_msgToInteractive___lambda__1___closed__1;
 x_2 = l_Lean_Widget_msgToInteractive___lambda__1___closed__2;
-x_3 = lean_unsigned_to_nat(138u);
+x_3 = lean_unsigned_to_nat(130u);
 x_4 = lean_unsigned_to_nat(6u);
 x_5 = l_Lean_Widget_msgToInteractive___lambda__1___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -16945,7 +16952,27 @@ x_6 = l_Lean_Widget_msgToInteractive(x_1, x_5, x_3, x_4);
 return x_6;
 }
 }
-static lean_object* _init_l_Lean_Widget_msgToInteractiveDiagnostic___lambda__1___closed__1() {
+LEAN_EXPORT lean_object* l_Lean_Widget_msgToInteractiveDiagnostic___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+_start:
+{
+lean_object* x_8; lean_object* x_9; lean_object* x_10; 
+x_8 = lean_box(0);
+x_9 = lean_alloc_ctor(0, 8, 0);
+lean_ctor_set(x_9, 0, x_1);
+lean_ctor_set(x_9, 1, x_2);
+lean_ctor_set(x_9, 2, x_3);
+lean_ctor_set(x_9, 3, x_8);
+lean_ctor_set(x_9, 4, x_4);
+lean_ctor_set(x_9, 5, x_6);
+lean_ctor_set(x_9, 6, x_5);
+lean_ctor_set(x_9, 7, x_8);
+x_10 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_10, 0, x_9);
+lean_ctor_set(x_10, 1, x_7);
+return x_10;
+}
+}
+static lean_object* _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__1() {
 _start:
 {
 lean_object* x_1; 
@ -16953,38 +16980,25 @@ x_1 = lean_mk_string_from_bytes("Lean 4", 6);
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Widget_msgToInteractiveDiagnostic___lambda__1___closed__2() {
+static lean_object* _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Widget_msgToInteractiveDiagnostic___lambda__1___closed__1;
+x_1 = l_Lean_Widget_msgToInteractiveDiagnostic___closed__1;
 x_2 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_2, 0, x_1);
 return x_2;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Widget_msgToInteractiveDiagnostic___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+static lean_object* _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__3() {
 _start:
 {
-lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; 
-x_6 = lean_box(0);
-x_7 = l_Lean_Widget_msgToInteractiveDiagnostic___lambda__1___closed__2;
-x_8 = lean_alloc_ctor(0, 8, 0);
-lean_ctor_set(x_8, 0, x_1);
-lean_ctor_set(x_8, 1, x_2);
-lean_ctor_set(x_8, 2, x_3);
-lean_ctor_set(x_8, 3, x_6);
-lean_ctor_set(x_8, 4, x_7);
-lean_ctor_set(x_8, 5, x_4);
-lean_ctor_set(x_8, 6, x_6);
-lean_ctor_set(x_8, 7, x_6);
-x_9 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_9, 0, x_8);
-lean_ctor_set(x_9, 1, x_5);
-return x_9;
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_MessageData_isDeprecationWarning___lambda__1___boxed), 1, 0);
+return x_1;
 }
 }
-static lean_object* _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__1() {
+static lean_object* _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__4() {
 _start:
 {
 lean_object* x_1; 
@ -16992,7 +17006,7 @@ x_1 = lean_mk_string_from_bytes("[error when printing message: ", 30);
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__2() {
+static lean_object* _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__5() {
 _start:
 {
 lean_object* x_1; 
@ -17000,43 +17014,69 @@ x_1 = lean_mk_string_from_bytes("]", 1);
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__3() {
+static lean_object* _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__6() {
 _start:
 {
-uint8_t x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = 2;
-x_2 = lean_box(x_1);
-x_3 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_3, 0, x_2);
-return x_3;
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_MessageData_isUnusedVariableWarning___lambda__1___boxed), 1, 0);
+return x_1;
 }
 }
-static lean_object* _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__4() {
+static lean_object* _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__7() {
 _start:
 {
-uint8_t x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = 1;
-x_2 = lean_box(x_1);
-x_3 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_3, 0, x_2);
-return x_3;
+lean_object* x_1; lean_object* x_2; 
+x_1 = lean_unsigned_to_nat(1u);
+x_2 = lean_mk_empty_array_with_capacity(x_1);
+return x_2;
 }
 }
-static lean_object* _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__5() {
+static lean_object* _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__8() {
 _start:
 {
-uint8_t x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = 0;
-x_2 = lean_box(x_1);
-x_3 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_3, 0, x_2);
-return x_3;
+lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l_Lean_Widget_msgToInteractiveDiagnostic___closed__7;
+x_2 = 0;
+x_3 = lean_box(x_2);
+x_4 = lean_array_push(x_1, x_3);
+return x_4;
+}
+}
+static lean_object* _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__9() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Widget_msgToInteractiveDiagnostic___closed__8;
+x_2 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
+static lean_object* _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__10() {
+_start:
+{
+lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l_Lean_Widget_msgToInteractiveDiagnostic___closed__7;
+x_2 = 1;
+x_3 = lean_box(x_2);
+x_4 = lean_array_push(x_1, x_3);
+return x_4;
+}
+}
+static lean_object* _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__11() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l_Lean_Widget_msgToInteractiveDiagnostic___closed__10;
+x_2 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
 }
 }
 LEAN_EXPORT lean_object* l_Lean_Widget_msgToInteractiveDiagnostic(lean_object* x_1, lean_object* x_2, uint8_t x_3, lean_object* x_4) {
 _start:
 {
-lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; 
 x_5 = lean_ctor_get(x_2, 1);
 lean_inc(x_5);
 lean_inc(x_5);
@ -17047,136 +17087,177 @@ x_8 = lean_ctor_get_uint8(x_2, sizeof(void*)*5);
 x_9 = lean_ctor_get(x_2, 4);
 lean_inc(x_9);
 lean_dec(x_2);
-x_10 = lean_unsigned_to_nat(0u);
-x_11 = l_Lean_Widget_msgToInteractive(x_9, x_3, x_10, x_4);
+x_10 = l_Lean_Widget_msgToInteractiveDiagnostic___closed__3;
+lean_inc(x_9);
+x_11 = l_Lean_MessageData_hasTag(x_10, x_9);
+x_12 = lean_unsigned_to_nat(0u);
+lean_inc(x_9);
+x_13 = l_Lean_Widget_msgToInteractive(x_9, x_3, x_12, x_4);
 if (lean_obj_tag(x_7) == 0)
 {
 lean_inc(x_5);
-x_12 = x_5;
-goto block_44;
+x_14 = x_5;
+goto block_57;
 }
 else
 {
-lean_object* x_45; 
-x_45 = lean_ctor_get(x_7, 0);
-lean_inc(x_45);
-x_12 = x_45;
-goto block_44;
+lean_object* x_58; 
+x_58 = lean_ctor_get(x_7, 0);
+lean_inc(x_58);
+x_14 = x_58;
+goto block_57;
 }
-block_44:
+block_57:
 {
-lean_object* x_13; lean_object* x_14; lean_object* x_15; 
-x_13 = l_Lean_FileMap_leanPosToLspPos(x_1, x_12);
+lean_object* x_15; lean_object* x_16; lean_object* x_17; 
+x_15 = l_Lean_FileMap_leanPosToLspPos(x_1, x_14);
 lean_inc(x_6);
-x_14 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_14, 0, x_6);
-lean_ctor_set(x_14, 1, x_13);
+x_16 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_16, 0, x_6);
+lean_ctor_set(x_16, 1, x_15);
 if (lean_obj_tag(x_7) == 0)
 {
 lean_dec(x_5);
 lean_dec(x_1);
 lean_inc(x_6);
-x_15 = x_6;
-goto block_34;
+x_17 = x_6;
+goto block_47;
 }
 else
 {
-lean_object* x_35; lean_object* x_36; lean_object* x_37; uint8_t x_38; 
-x_35 = lean_ctor_get(x_7, 0);
-lean_inc(x_35);
+lean_object* x_48; lean_object* x_49; lean_object* x_50; uint8_t x_51; 
+x_48 = lean_ctor_get(x_7, 0);
+lean_inc(x_48);
 lean_dec(x_7);
-x_36 = lean_ctor_get(x_5, 0);
-lean_inc(x_36);
+x_49 = lean_ctor_get(x_5, 0);
+lean_inc(x_49);
 lean_dec(x_5);
-x_37 = lean_ctor_get(x_35, 0);
-lean_inc(x_37);
-x_38 = lean_nat_dec_lt(x_36, x_37);
-lean_dec(x_37);
-if (x_38 == 0)
+x_50 = lean_ctor_get(x_48, 0);
+lean_inc(x_50);
+x_51 = lean_nat_dec_lt(x_49, x_50);
+lean_dec(x_50);
+if (x_51 == 0)
 {
-lean_object* x_39; 
-lean_dec(x_36);
-x_39 = l_Lean_FileMap_leanPosToLspPos(x_1, x_35);
+lean_object* x_52; 
+lean_dec(x_49);
+x_52 = l_Lean_FileMap_leanPosToLspPos(x_1, x_48);
 lean_dec(x_1);
-x_15 = x_39;
-goto block_34;
+x_17 = x_52;
+goto block_47;
 }
 else
 {
-lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; 
-lean_dec(x_35);
-x_40 = lean_unsigned_to_nat(1u);
-x_41 = lean_nat_add(x_36, x_40);
-lean_dec(x_36);
-x_42 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_42, 0, x_41);
-lean_ctor_set(x_42, 1, x_10);
-x_43 = l_Lean_FileMap_leanPosToLspPos(x_1, x_42);
+lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; 
+lean_dec(x_48);
+x_53 = lean_unsigned_to_nat(1u);
+x_54 = lean_nat_add(x_49, x_53);
+lean_dec(x_49);
+x_55 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_55, 0, x_54);
+lean_ctor_set(x_55, 1, x_12);
+x_56 = l_Lean_FileMap_leanPosToLspPos(x_1, x_55);
 lean_dec(x_1);
-x_15 = x_43;
-goto block_34;
+x_17 = x_56;
+goto block_47;
 }
 }
-block_34:
+block_47:
 {
-lean_object* x_16; lean_object* x_17; 
-x_16 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_16, 0, x_6);
-lean_ctor_set(x_16, 1, x_15);
+lean_object* x_18; uint8_t x_19; 
+x_18 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_18, 0, x_6);
+lean_ctor_set(x_18, 1, x_17);
 switch (x_8) {
 case 0:
 {
-lean_object* x_31; 
-x_31 = l_Lean_Widget_msgToInteractiveDiagnostic___closed__3;
-x_17 = x_31;
-goto block_30;
+uint8_t x_44; 
+x_44 = 2;
+x_19 = x_44;
+goto block_43;
 }
 case 1:
 {
-lean_object* x_32; 
-x_32 = l_Lean_Widget_msgToInteractiveDiagnostic___closed__4;
-x_17 = x_32;
-goto block_30;
+uint8_t x_45; 
+x_45 = 1;
+x_19 = x_45;
+goto block_43;
 }
 default: 
 {
-lean_object* x_33; 
-x_33 = l_Lean_Widget_msgToInteractiveDiagnostic___closed__5;
-x_17 = x_33;
-goto block_30;
+uint8_t x_46; 
+x_46 = 0;
+x_19 = x_46;
+goto block_43;
 }
 }
-block_30:
+block_43:
 {
-if (lean_obj_tag(x_11) == 0)
+lean_object* x_20; lean_object* x_21; lean_object* x_22; 
+x_20 = lean_box(x_19);
+x_21 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_21, 0, x_20);
+if (x_11 == 0)
 {
-lean_object* x_18; lean_object* x_19; lean_object* x_20; 
-x_18 = lean_ctor_get(x_11, 0);
-lean_inc(x_18);
-x_19 = lean_ctor_get(x_11, 1);
-lean_inc(x_19);
-lean_dec(x_11);
-x_20 = l_Lean_Widget_msgToInteractiveDiagnostic___lambda__1(x_16, x_14, x_17, x_18, x_19);
-return x_20;
+lean_object* x_38; uint8_t x_39; 
+x_38 = l_Lean_Widget_msgToInteractiveDiagnostic___closed__6;
+x_39 = l_Lean_MessageData_hasTag(x_38, x_9);
+if (x_39 == 0)
+{
+lean_object* x_40; 
+x_40 = lean_box(0);
+x_22 = x_40;
+goto block_37;
 }
 else
 {
-lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; 
-x_21 = lean_ctor_get(x_11, 0);
-lean_inc(x_21);
-x_22 = lean_ctor_get(x_11, 1);
-lean_inc(x_22);
-lean_dec(x_11);
-x_23 = lean_io_error_to_string(x_21);
-x_24 = l_Lean_Widget_msgToInteractiveDiagnostic___closed__1;
-x_25 = lean_string_append(x_24, x_23);
-lean_dec(x_23);
-x_26 = l_Lean_Widget_msgToInteractiveDiagnostic___closed__2;
-x_27 = lean_string_append(x_25, x_26);
-x_28 = lean_alloc_ctor(0, 1, 0);
-lean_ctor_set(x_28, 0, x_27);
-x_29 = l_Lean_Widget_msgToInteractiveDiagnostic___lambda__1(x_16, x_14, x_17, x_28, x_22);
-return x_29;
+lean_object* x_41; 
+x_41 = l_Lean_Widget_msgToInteractiveDiagnostic___closed__9;
+x_22 = x_41;
+goto block_37;
+}
+}
+else
+{
+lean_object* x_42; 
+lean_dec(x_9);
+x_42 = l_Lean_Widget_msgToInteractiveDiagnostic___closed__11;
+x_22 = x_42;
+goto block_37;
+}
+block_37:
+{
+if (lean_obj_tag(x_13) == 0)
+{
+lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; 
+x_23 = lean_ctor_get(x_13, 0);
+lean_inc(x_23);
+x_24 = lean_ctor_get(x_13, 1);
+lean_inc(x_24);
+lean_dec(x_13);
+x_25 = l_Lean_Widget_msgToInteractiveDiagnostic___closed__2;
+x_26 = l_Lean_Widget_msgToInteractiveDiagnostic___lambda__1(x_18, x_16, x_21, x_25, x_22, x_23, x_24);
+return x_26;
+}
+else
+{
+lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; 
+x_27 = lean_ctor_get(x_13, 0);
+lean_inc(x_27);
+x_28 = lean_ctor_get(x_13, 1);
+lean_inc(x_28);
+lean_dec(x_13);
+x_29 = lean_io_error_to_string(x_27);
+x_30 = l_Lean_Widget_msgToInteractiveDiagnostic___closed__4;
+x_31 = lean_string_append(x_30, x_29);
+lean_dec(x_29);
+x_32 = l_Lean_Widget_msgToInteractiveDiagnostic___closed__5;
+x_33 = lean_string_append(x_31, x_32);
+x_34 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_34, 0, x_33);
+x_35 = l_Lean_Widget_msgToInteractiveDiagnostic___closed__2;
+x_36 = l_Lean_Widget_msgToInteractiveDiagnostic___lambda__1(x_18, x_16, x_21, x_35, x_22, x_34, x_28);
+return x_36;
+}
 }
 }
 }
@ -17194,14 +17275,8 @@ return x_6;
 }
 }
 lean_object* initialize_Init(uint8_t builtin, lean_object*);
-lean_object* initialize_Lean_Data_Lsp(uint8_t builtin, lean_object*);
-lean_object* initialize_Lean_Message(uint8_t builtin, lean_object*);
-lean_object* initialize_Lean_Elab_InfoTree(uint8_t builtin, lean_object*);
+lean_object* initialize_Lean_Linter_UnusedVariables(uint8_t builtin, lean_object*);
 lean_object* initialize_Lean_Server_Utils(uint8_t builtin, lean_object*);
-lean_object* initialize_Lean_Server_Rpc_Basic(uint8_t builtin, lean_object*);
-lean_object* initialize_Lean_Widget_Basic(uint8_t builtin, lean_object*);
-lean_object* initialize_Lean_Widget_TaggedText(uint8_t builtin, lean_object*);
-lean_object* initialize_Lean_Widget_InteractiveCode(uint8_t builtin, lean_object*);
 lean_object* initialize_Lean_Widget_InteractiveGoal(uint8_t builtin, lean_object*);
 static bool _G_initialized = false;
 LEAN_EXPORT lean_object* initialize_Lean_Widget_InteractiveDiagnostic(uint8_t builtin, lean_object* w) {
@ -17211,30 +17286,12 @@ _G_initialized = true;
 res = initialize_Init(builtin, lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-res = initialize_Lean_Data_Lsp(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-res = initialize_Lean_Message(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-res = initialize_Lean_Elab_InfoTree(builtin, lean_io_mk_world());
+res = initialize_Lean_Linter_UnusedVariables(builtin, lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 res = initialize_Lean_Server_Utils(builtin, lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-res = initialize_Lean_Server_Rpc_Basic(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-res = initialize_Lean_Widget_Basic(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-res = initialize_Lean_Widget_TaggedText(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
-res = initialize_Lean_Widget_InteractiveCode(builtin, lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-lean_dec_ref(res);
 res = initialize_Lean_Widget_InteractiveGoal(builtin, lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
@ -17381,10 +17438,6 @@ l_Lean_Widget_msgToInteractive___lambda__1___closed__3 = _init_l_Lean_Widget_msg
 lean_mark_persistent(l_Lean_Widget_msgToInteractive___lambda__1___closed__3);
 l_Lean_Widget_msgToInteractive___lambda__1___closed__4 = _init_l_Lean_Widget_msgToInteractive___lambda__1___closed__4();
 lean_mark_persistent(l_Lean_Widget_msgToInteractive___lambda__1___closed__4);
-l_Lean_Widget_msgToInteractiveDiagnostic___lambda__1___closed__1 = _init_l_Lean_Widget_msgToInteractiveDiagnostic___lambda__1___closed__1();
-lean_mark_persistent(l_Lean_Widget_msgToInteractiveDiagnostic___lambda__1___closed__1);
-l_Lean_Widget_msgToInteractiveDiagnostic___lambda__1___closed__2 = _init_l_Lean_Widget_msgToInteractiveDiagnostic___lambda__1___closed__2();
-lean_mark_persistent(l_Lean_Widget_msgToInteractiveDiagnostic___lambda__1___closed__2);
 l_Lean_Widget_msgToInteractiveDiagnostic___closed__1 = _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__1();
 lean_mark_persistent(l_Lean_Widget_msgToInteractiveDiagnostic___closed__1);
 l_Lean_Widget_msgToInteractiveDiagnostic___closed__2 = _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__2();
@ -17395,6 +17448,18 @@ l_Lean_Widget_msgToInteractiveDiagnostic___closed__4 = _init_l_Lean_Widget_msgTo
 lean_mark_persistent(l_Lean_Widget_msgToInteractiveDiagnostic___closed__4);
 l_Lean_Widget_msgToInteractiveDiagnostic___closed__5 = _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__5();
 lean_mark_persistent(l_Lean_Widget_msgToInteractiveDiagnostic___closed__5);
+l_Lean_Widget_msgToInteractiveDiagnostic___closed__6 = _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__6();
+lean_mark_persistent(l_Lean_Widget_msgToInteractiveDiagnostic___closed__6);
+l_Lean_Widget_msgToInteractiveDiagnostic___closed__7 = _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__7();
+lean_mark_persistent(l_Lean_Widget_msgToInteractiveDiagnostic___closed__7);
+l_Lean_Widget_msgToInteractiveDiagnostic___closed__8 = _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__8();
+lean_mark_persistent(l_Lean_Widget_msgToInteractiveDiagnostic___closed__8);
+l_Lean_Widget_msgToInteractiveDiagnostic___closed__9 = _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__9();
+lean_mark_persistent(l_Lean_Widget_msgToInteractiveDiagnostic___closed__9);
+l_Lean_Widget_msgToInteractiveDiagnostic___closed__10 = _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__10();
+lean_mark_persistent(l_Lean_Widget_msgToInteractiveDiagnostic___closed__10);
+l_Lean_Widget_msgToInteractiveDiagnostic___closed__11 = _init_l_Lean_Widget_msgToInteractiveDiagnostic___closed__11();
+lean_mark_persistent(l_Lean_Widget_msgToInteractiveDiagnostic___closed__11);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus