chore: update stage0

2021-05-14 18:07:47 -07:00 · 2021-05-14 18:07:47 -07:00 · 16ef336b99
commit 16ef336b99
parent dbe0d2d706
35 changed files with 10513 additions and 4310 deletions
--- a/stage0/src/Lean/Data/Options.lean
+++ b/stage0/src/Lean/Data/Options.lean
@ -13,6 +13,7 @@ def Options.empty : Options  := {}
 instance : Inhabited Options where
  default := {}
 instance : ToString Options := inferInstanceAs (ToString KVMap)
+instance : ForIn m Options (Name × DataValue) := inferInstanceAs (ForIn _ KVMap _)

 structure OptionDecl where
  defValue : DataValue
@ -112,6 +113,9 @@ protected structure Decl (α : Type) where
  group    : String := ""
  descr    : String := ""

+protected def get? [KVMap.Value α] (opts : Options) (opt : Lean.Option α) : Option α :=
+  opts.get? opt.name
+
 protected def get [KVMap.Value α] (opts : Options) (opt : Lean.Option α) : α :=
  opts.get opt.name opt.defValue

--- a/stage0/src/Lean/Elab.lean
+++ b/stage0/src/Lean/Elab.lean
@ -28,3 +28,4 @@ import Lean.Elab.PreDefinition
 import Lean.Elab.Deriving
 import Lean.Elab.DeclarationRange
 import Lean.Elab.Extra
+import Lean.Elab.GenInjective
--- a/stage0/src/Lean/Elab/GenInjective.lean
+++ b/stage0/src/Lean/Elab/GenInjective.lean
@ -0,0 +1,16 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Elab.Command
+import Lean.Meta.Injective
+
+namespace Lean.Elab.Command
+
+@[builtinCommandElab genInjectiveTheorems] def elabGenInjectiveTheorems : CommandElab := fun stx => do
+  let declName ← resolveGlobalConstNoOverload stx[1].getId
+  liftTermElabM none do
+    Meta.mkInjectiveTheorems declName
+
+end Lean.Elab.Command
--- a/stage0/src/Lean/Elab/Inductive.lean
+++ b/stage0/src/Lean/Elab/Inductive.lean
@ -9,6 +9,7 @@ import Lean.Util.CollectLevelParams
 import Lean.Util.Constructions
 import Lean.Meta.CollectFVars
 import Lean.Meta.SizeOf
+import Lean.Meta.Injective
 import Lean.Meta.IndPredBelow
 import Lean.Elab.Command
 import Lean.Elab.DefView
@ -519,6 +520,8 @@ def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do
    mkInductiveDecl vars views
    mkSizeOfInstances view0.declName
    Lean.Meta.IndPredBelow.mkBelow view0.declName
+    for view in views do
+      mkInjectiveTheorems view.declName
  applyDerivingHandlers views

 end Lean.Elab.Command
--- a/stage0/src/Lean/Elab/Structure.lean
+++ b/stage0/src/Lean/Elab/Structure.lean
@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 import Lean.Parser.Command
 import Lean.Meta.Closure
 import Lean.Meta.SizeOf
+import Lean.Meta.Injective
 import Lean.Elab.Command
 import Lean.Elab.DeclModifiers
 import Lean.Elab.DeclUtil
@ -581,6 +582,7 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
            }
            unless isClass do
              mkSizeOfInstances declName
+              mkInjectiveTheorems declName
            return declName
  derivingClassViews.forM fun view => view.applyHandlers #[declName]

--- a/stage0/src/Lean/Meta/Injective.lean
+++ b/stage0/src/Lean/Meta/Injective.lean
@ -5,24 +5,27 @@ Authors: Leonardo de Moura
 -/
 import Lean.Meta.Tactic.Injection
 import Lean.Meta.Tactic.Apply
-import Lean.Meta.Tactic.Simp.SimpAll
+import Lean.Meta.Tactic.Cases
+import Lean.Meta.Tactic.Subst
+import Lean.Meta.Tactic.Simp.Types
+import Lean.Meta.Tactic.Assumption

 namespace Lean.Meta

-private def mkAnd (args : Array Expr) : Expr := do
+private def mkAnd? (args : Array Expr) : Option Expr := do
  if args.isEmpty then
-    return mkConst ``True
+    return none
  else
    let mut result := args.back
    for arg in args.reverse[1:] do
      result := mkApp2 (mkConst ``And) arg result
    return result

-private partial def mkInjectiveTheoremTypeCore (ctorVal : ConstructorVal) (useEq : Bool) : MetaM Expr := do
+private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useEq : Bool) : MetaM (Option Expr) := do
  let us := ctorVal.levelParams.map mkLevelParam
  forallBoundedTelescope ctorVal.type ctorVal.numParams fun params type =>
  forallTelescope type fun args1 resultType => do
-    let jp (args2 args2New : Array Expr) : MetaM Expr := do
+    let jp (args2 args2New : Array Expr) : MetaM (Option Expr) := do
      let lhs := mkAppN (mkAppN (mkConst ctorVal.name us) params) args1
      let rhs := mkAppN (mkAppN (mkConst ctorVal.name us) params) args2
      let eq ← mkEq lhs rhs
@ -34,14 +37,16 @@ private partial def mkInjectiveTheoremTypeCore (ctorVal : ConstructorVal) (useEq
            eqs := eqs.push (← mkEq arg1 arg2)
          else
            eqs := eqs.push (← mkHEq arg1 arg2)
-      let andEqs := mkAnd eqs
-      let result ←
-        if useEq then
-          mkEq eq andEqs
-        else
-          mkArrow eq andEqs
-      mkForallFVars params (← mkForallFVars args1 (← mkForallFVars args2New result))
-    let rec mkArgs2 (i : Nat) (type : Expr) (args2 args2New : Array Expr) : MetaM Expr := do
+      if let some andEqs ← mkAnd? eqs then
+        let result ←
+          if useEq then
+            mkEq eq andEqs
+          else
+            mkArrow eq andEqs
+        mkForallFVars params (← mkForallFVars args1 (← mkForallFVars args2New result))
+      else
+        return none
+    let rec mkArgs2 (i : Nat) (type : Expr) (args2 args2New : Array Expr) : MetaM (Option Expr) := do
      if h : i < args1.size then
        match (← whnf type) with
        | Expr.forallE n d b _ =>
@ -61,31 +66,35 @@ private partial def mkInjectiveTheoremTypeCore (ctorVal : ConstructorVal) (useEq
      withNewBinderInfos (args1.map fun arg1 => (arg1.fvarId!, BinderInfo.implicit)) <|
        mkArgs2 0 type #[] #[]

-private def mkInjectiveTheoremType (ctorVal : ConstructorVal) : MetaM Expr :=
-  mkInjectiveTheoremTypeCore ctorVal false
+private def mkInjectiveTheoremType? (ctorVal : ConstructorVal) : MetaM (Option Expr) :=
+  mkInjectiveTheoremTypeCore? ctorVal false
+
+private def injTheoremFailureHeader (ctorName : Name) : MessageData :=
+  m!"failed to prove injectivity theorem for constructor '{ctorName}', use 'set_option genInjectivity false' to disable the generation"

 private def throwInjectiveTheoremFailure {α} (ctorName : Name) (mvarId : MVarId) : MetaM α :=
-  throwError "failed to prove injective theorem for constructor '{ctorName}', use 'set_option genInjective false' to disable the generation{indentD <| MessageData.ofGoal mvarId}"
+  throwError "{injTheoremFailureHeader ctorName}{indentD <| MessageData.ofGoal mvarId}"

-private def simpAllInj (ctorName : Name) (mvarId : MVarId) : MetaM Unit := do
-  match (← simpAll mvarId (← Simp.Context.mkDefault)) with
-  | none => pure ()
-  | some mvarId => throwInjectiveTheoremFailure ctorName mvarId
+private def solveEqOfCtorEq (ctorName : Name) (mvarId : MVarId) (h : FVarId) : MetaM Unit := do
+  match (← injection mvarId h) with
+  | InjectionResult.solved => unreachable!
+  | InjectionResult.subgoal mvarId .. =>
+    (← splitAnd mvarId).forM fun mvarId =>
+      unless (← assumptionCore mvarId) do
+        throwInjectiveTheoremFailure ctorName mvarId

 private def mkInjectiveTheoremValue (ctorName : Name) (targetType : Expr) : MetaM Expr :=
  forallTelescopeReducing targetType fun xs type => do
    let mvar ← mkFreshExprSyntheticOpaqueMVar type
-    match (← injection mvar.mvarId! xs.back.fvarId!) with
-    | InjectionResult.solved => mkLambdaFVars xs mvar
-    | InjectionResult.subgoal mvarId .. =>
-      simpAllInj ctorName mvarId
-      mkLambdaFVars xs mvar
+    solveEqOfCtorEq ctorName mvar.mvarId! xs.back.fvarId!
+    mkLambdaFVars xs mvar

 def mkInjectiveTheoremNameFor (ctorName : Name) : Name :=
  ctorName ++ `inj

 private def mkInjectiveTheorem (ctorVal : ConstructorVal) : MetaM Unit := do
-  let type  ← mkInjectiveTheoremType ctorVal
+  let some type ← mkInjectiveTheoremType? ctorVal
+    | return ()
  let value ← mkInjectiveTheoremValue ctorVal.name type
  addDecl <| Declaration.thmDecl {
    name        := mkInjectiveTheoremNameFor ctorVal.name
@ -97,8 +106,8 @@ private def mkInjectiveTheorem (ctorVal : ConstructorVal) : MetaM Unit := do
 def mkInjectiveEqTheoremNameFor (ctorName : Name) : Name :=
  ctorName ++ `injEq

-private def mkInjectiveEqTheoremType (ctorVal : ConstructorVal) : MetaM Expr :=
-  mkInjectiveTheoremTypeCore ctorVal true
+private def mkInjectiveEqTheoremType? (ctorVal : ConstructorVal) : MetaM (Option Expr) :=
+  mkInjectiveTheoremTypeCore? ctorVal true

 private def mkInjectiveEqTheoremValue (ctorName : Name) (targetType : Expr) : MetaM Expr := do
  forallTelescopeReducing targetType fun xs type => do
@ -107,15 +116,15 @@ private def mkInjectiveEqTheoremValue (ctorName : Name) (targetType : Expr) : Me
      | throwError "unexpected number of subgoals when proving injective theorem for constructor '{ctorName}'"
    let (h, mvarId₁) ← intro1 mvarId₁
    let (_, mvarId₂) ← intro1 mvarId₂
-    simpAllInj ctorName mvarId₂
-    match (← injection mvarId₁ h) with
-    | InjectionResult.solved => mkLambdaFVars xs mvar
-    | InjectionResult.subgoal mvarId .. =>
-      simpAllInj ctorName mvarId
-      mkLambdaFVars xs mvar
+    solveEqOfCtorEq ctorName mvarId₁ h
+    let mvarId₂ ← casesAnd mvarId₂
+    let mvarId₂ ← substEqs mvarId₂
+    applyRefl mvarId₂ (injTheoremFailureHeader ctorName)
+    mkLambdaFVars xs mvar

 private def mkInjectiveEqTheorem (ctorVal : ConstructorVal) : MetaM Unit := do
-  let type  ← mkInjectiveEqTheoremType ctorVal
+  let some type ← mkInjectiveEqTheoremType? ctorVal
+    | return ()
  let value ← mkInjectiveEqTheoremValue ctorVal.name type
  let name := mkInjectiveEqTheoremNameFor ctorVal.name
  addDecl <| Declaration.thmDecl {
@ -126,18 +135,19 @@ private def mkInjectiveEqTheorem (ctorVal : ConstructorVal) : MetaM Unit := do
  }
  addSimpLemma name (post := true) AttributeKind.global (prio := eval_prio default)

-register_builtin_option genInjective : Bool := {
+register_builtin_option genInjectivity : Bool := {
  defValue := true
-  descr    := "generate injective theorems for inductive datatype constructors"
+  descr    := "generate injectivity theorems for inductive datatype constructors"
 }

 def mkInjectiveTheorems (declName : Name) : MetaM Unit := do
-  if (← getEnv).contains ``Eq.propIntro && genInjective.get (← getOptions) &&  !(← isInductivePredicate declName) then
+  if (← getEnv).contains ``Eq.propIntro && genInjectivity.get (← getOptions) &&  !(← isInductivePredicate declName) then
    let info ← getConstInfoInduct declName
-    for ctor in info.ctors do
-      let ctorVal ← getConstInfoCtor ctor
-      if ctorVal.numFields > 0 then
-        mkInjectiveTheorem ctorVal
-        mkInjectiveEqTheorem ctorVal
+    unless info.isUnsafe do
+      for ctor in info.ctors do
+        let ctorVal ← getConstInfoCtor ctor
+        if ctorVal.numFields > 0 then
+          mkInjectiveTheorem ctorVal
+          mkInjectiveEqTheorem ctorVal

 end Lean.Meta
--- a/stage0/src/Lean/Meta/Tactic/Apply.lean
+++ b/stage0/src/Lean/Meta/Tactic/Apply.lean
@ -97,4 +97,13 @@ def apply (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) :=
    result.forM headBetaMVarType
    return result

+def splitAnd (mvarId : MVarId) : MetaM (List MVarId) := do
+  saturate mvarId fun mvarId =>
+    observing? <| apply mvarId (mkConst ``And.intro)
+
+def applyRefl (mvarId : MVarId) (msg : MessageData) : MetaM Unit :=
+  withMVarContext mvarId do
+    let some [] ← observing? do apply mvarId (mkConst ``Eq.refl [← mkFreshLevelMVar])
+      | throwTacticEx `refl mvarId msg
+
 end Lean.Meta
--- a/stage0/src/Lean/Meta/Tactic/Cases.lean
+++ b/stage0/src/Lean/Meta/Tactic/Cases.lean
@ -321,6 +321,28 @@ end Cases
 def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNames := #[]) : MetaM (Array CasesSubgoal) :=
  Cases.cases mvarId majorFVarId givenNames

+def casesRec (mvarId : MVarId) (p : LocalDecl → MetaM Bool) : MetaM (List MVarId) :=
+  saturate mvarId fun mvarId =>
+    withMVarContext mvarId do
+      for localDecl in (← getLCtx) do
+        if (← p localDecl) then
+          let r? ← observing? do
+            let r ← cases mvarId localDecl.fvarId
+            return r.toList.map (·.mvarId)
+          if r?.isSome then
+            return r?
+      return none
+
+def casesAnd (mvarId : MVarId) : MetaM MVarId := do
+  let mvarIds ← casesRec mvarId fun localDecl => return (← instantiateMVars localDecl.type).isAppOfArity ``And 2
+  exactlyOne mvarIds
+
+def substEqs (mvarId : MVarId) : MetaM MVarId := do
+  let mvarIds ← casesRec mvarId fun localDecl => do
+    let type ← instantiateMVars localDecl.type
+    return type.isEq || type.isHEq
+  exactlyOne mvarIds
+
 builtin_initialize registerTraceClass `Meta.Tactic.cases

 end Lean.Meta
--- a/stage0/src/Lean/Meta/Tactic/Util.lean
+++ b/stage0/src/Lean/Meta/Tactic/Util.lean
@ -87,4 +87,25 @@ where
      get
    visit |>.run' candidates

+partial def saturate (mvarId : MVarId) (x : MVarId → MetaM (Option (List MVarId))) : MetaM (List MVarId) := do
+  let (_, r) ← go mvarId |>.run #[]
+  return r.toList
+where
+  go (mvarId : MVarId) : StateRefT (Array MVarId) MetaM Unit :=
+    withIncRecDepth do
+      match (← x mvarId) with
+      | none => modify fun s => s.push mvarId
+      | some mvarIds => mvarIds.forM go
+
+def exactlyOne (mvarIds : List MVarId) (msg : MessageData := "unexpected number of goals") : MetaM MVarId :=
+  match mvarIds with
+  | [mvarId] => return mvarId
+  | _        => throwError msg
+
+def ensureAtMostOne (mvarIds : List MVarId) (msg : MessageData := "unexpected number of goals") : MetaM (Option MVarId) :=
+  match mvarIds with
+  | []       => return none
+  | [mvarId] => return some mvarId
+  | _        => throwError msg
+
 end Lean.Meta
--- a/stage0/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/stage0/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@ -96,6 +96,17 @@ register_builtin_option pp.safe_shadowing  : Bool := {
  group    := "pp"
  descr    := "(pretty printer) allow variable shadowing if there is no collision"
 }
+register_builtin_option pp.proofs : Bool := {
+  defValue := false
+  group    := "pp"
+  descr    := "(pretty printer) if set to false, replace proofs appearing as an argument to a function with a placeholder"
+}
+register_builtin_option pp.proofs.withType : Bool := {
+  defValue := true
+  group    := "pp"
+  descr    := "(pretty printer) when eliding a proof (see `pp.proofs`), show its type instead"
+}
+
 -- TODO:
 /-
 register_builtin_option g_pp_max_depth : Nat := {
@ -108,11 +119,6 @@ register_builtin_option g_pp_max_steps : Nat := {
  group    := "pp"
  descr    := "(pretty printer) maximum number of visited expressions, after that it will use ellipsis"
 }
-register_builtin_option g_pp_proofs : Bool := {
-  defValue := false
-  group    := "pp"
-  descr    := "(pretty printer) if set to false, the type will be displayed instead of the value for every proof appearing as an argument to a function"
-}
 register_builtin_option g_pp_locals_full_names : Bool := {
  defValue := false
  group    := "pp"
@ -163,6 +169,8 @@ def getPPFullNames (o : Options) : Bool := o.get `pp.full_names (getPPAll o)
 def getPPPrivateNames (o : Options) : Bool := o.get `pp.private_names (getPPAll o)
 def getPPUnicode (o : Options) : Bool := o.get `pp.unicode true
 def getPPSafeShadowing (o : Options) : Bool := o.get `pp.safe_shadowing true
+def getPPProofs (o : Options) : Bool := o.get pp.proofs.name (getPPAll o)
+def getPPProofsWithType (o : Options) : Bool := o.get pp.proofs.withType.name true

 /-- Associate pretty printer options to a specific subterm using a synthetic position. -/
 abbrev OptionsPerPos := Std.RBMap Nat Options compare
@ -255,7 +263,10 @@ def getExprKind : DelabM Name := do
 /-- Evaluate option accessor, using subterm-specific options if set. -/
 def getPPOption (opt : Options → Bool) : DelabM Bool := do
  let ctx ← read
-  let opts ← ctx.optionsPerPos.find? ctx.pos |>.getD ctx.defaultOptions
+  let mut opts := ctx.defaultOptions
+  if let some opts' ← ctx.optionsPerPos.find? ctx.pos then
+    for (k, v) in opts' do
+      opts := opts.insert k v
  return opt opts

 def whenPPOption (opt : Options → Bool) (d : Delab) : Delab := do
@ -361,7 +372,19 @@ partial def delabFor : Name → Delab
      -- have `app.Option.some` fall back to `app` etc.
      delabFor k.getRoot

-def delab : Delab := do
+partial def delab : Delab := do
+  unless (← getPPOption getPPProofs) do
+    let e ← getExpr
+    -- no need to hide atomic proofs
+    unless e.isAtomic do
+      try
+        let ty ← Meta.inferType (← getExpr)
+        if ← Meta.isProp ty then
+          if ← getPPOption getPPProofsWithType then
+            return ← ``((_ : $(← descend ty 0 delab)))
+          else
+            return ← ``(_)
+      catch _ => pure ()
  let k ← getExprKind
  delabFor k <|> (liftM $ show MetaM Syntax from throwError "don't know how to delaborate '{k}'")

@ -382,7 +405,14 @@ end Delaborator
 /-- "Delaborate" the given term into surface-level syntax using the default and given subterm-specific options. -/
 def delab (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (optionsPerPos : OptionsPerPos := {}) : MetaM Syntax := do
  trace[PrettyPrinter.delab.input] "{fmt e}"
-  let opts ← MonadOptions.getOptions
+  let mut opts ← MonadOptions.getOptions
+  -- default `pp.proofs` to `true` if `e` is a proof
+  if pp.proofs.get? opts == none then
+    try
+      let ty ← Meta.inferType e
+      if ← Meta.isProp ty then
+        opts := pp.proofs.set opts true
+    catch _ => pure ()
  catchInternalId Delaborator.delabFailureId
    (Delaborator.delab.run { expr := e, defaultOptions := opts, optionsPerPos := optionsPerPos, currNamespace := currNamespace, openDecls := openDecls })
    (fun _ => unreachable!)
--- a/stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@ -611,16 +611,27 @@ partial def delabDoElems : DelabM (List Syntax) := do

@[builtinDelab app.Bind.bind]
 def delabDo : Delab := whenPPOption getPPNotation do
-  unless (← getExpr).isAppOfArity `Bind.bind 6 do
-    failure
+  guard <| (← getExpr).isAppOfArity `Bind.bind 6
  let elems ← delabDoElems
  let items ← elems.toArray.mapM (`(doSeqItem|$(·):doElem))
  `(do $items:doSeqItem*)

@[builtinDelab app.sorryAx]
 def delabSorryAx : Delab := whenPPOption getPPNotation do
-  unless (← getExpr).isAppOfArity ``sorryAx 2 do
-    failure
+  guard <| (← getExpr).isAppOfArity ``sorryAx 2
  `(sorry)

+@[builtinDelab app.Eq.ndrec]
+def delabEqNDRec : Delab := whenPPOption getPPNotation do
+  guard <| (← getExpr).getAppNumArgs == 6
+  -- Eq.ndrec.{u1, u2} : {α : Sort u2} → {a : α} → {motive : α → Sort u1} → (m : motive a) → {b : α} → (h : a = b) → motive b
+  let m ← withAppFn <| withAppFn <| withAppArg delab
+  let h ← withAppArg delab
+  `($h ▸ $m)
+
+@[builtinDelab app.Eq.rec]
+def delabEqRec : Delab := whenPPOption getPPNotation do
+  -- relevant signature parts as in `Eq.ndrec`
+  delabEqNDRec
+
 end Lean.PrettyPrinter.Delaborator
--- a/stage0/src/Lean/Server/FileWorker.lean
+++ b/stage0/src/Lean/Server/FileWorker.lean
@ -94,21 +94,6 @@ end Utils

 /- Asynchronous snapshot elaboration. -/
 section Elab
-  def publishDiagnostics (m : DocumentMeta) (diagnostics : Array Lsp.Diagnostic) (hOut : FS.Stream) : IO Unit :=
-    hOut.writeLspNotification {
-      method := "textDocument/publishDiagnostics"
-      param  := {
-        uri         := m.uri
-        version?    := m.version
-        diagnostics := diagnostics
-        : PublishDiagnosticsParams
-      }
-    }
-
-  def publishMessages (m : DocumentMeta) (msgLog : MessageLog) (hOut : FS.Stream) : IO Unit := do
-    let diagnostics ← msgLog.msgs.mapM (msgToDiagnostic m.text)
-    publishDiagnostics m diagnostics.toArray hOut
-
  /-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/
  private def nextCmdSnap (m : DocumentMeta) (parentSnap : Snapshot) (cancelTk : CancelToken) (hOut : FS.Stream)
  : ExceptT ElabTaskError IO Snapshot := do
--- a/stage0/src/Lean/Server/Utils.lean
+++ b/stage0/src/Lean/Server/Utils.lean
@ -121,6 +121,21 @@ def foldDocumentChanges (changes : @& Array Lsp.TextDocumentContentChangeEvent)
  -- NOTE: We assume Lean files are below 16 EiB.
  changes.foldl accumulateChanges (oldText, 0xffffffff)

+def publishDiagnostics (m : DocumentMeta) (diagnostics : Array Lsp.Diagnostic) (hOut : FS.Stream) : IO Unit :=
+  hOut.writeLspNotification {
+    method := "textDocument/publishDiagnostics"
+    param  := {
+      uri         := m.uri
+      version?    := m.version
+      diagnostics := diagnostics
+      : PublishDiagnosticsParams
+    }
+  }
+
+def publishMessages (m : DocumentMeta) (msgLog : MessageLog) (hOut : FS.Stream) : IO Unit := do
+  let diagnostics ← msgLog.msgs.mapM (msgToDiagnostic m.text)
+  publishDiagnostics m diagnostics.toArray hOut
+
 end Lean.Server

 namespace List
--- a/stage0/src/Lean/Server/Watchdog.lean
+++ b/stage0/src/Lean/Server/Watchdog.lean
@ -229,6 +229,7 @@ section ServerM
      | Except.error e => WorkerEvent.ioError e

  def startFileWorker (m : DocumentMeta) : ServerM Unit := do
+    publishDiagnostics m #[{ range := ⟨⟨0, 0⟩, ⟨0, 0⟩⟩, severity? := DiagnosticSeverity.information, message := "starting new server for file..." }] (← read).hOut
    let st ← read
    let headerAst ← parseHeaderAst m.text.source
    let workerProc ← Process.spawn {
--- a/stage0/stdlib/CMakeLists.txt
+++ b/stage0/stdlib/CMakeLists.txt
--- a/stage0/stdlib/Lean/Data/Options.c
+++ b/stage0/stdlib/Lean/Data/Options.c
@ -17,6 +17,7 @@ lean_object* l_Lean_getBoolOption___rarg(lean_object*, lean_object*, lean_object
 extern lean_object* l_Lean_Name_toString___closed__1;
 lean_object* l_Lean_KVMap_setBool(lean_object*, lean_object*, uint8_t);
 lean_object* l_Lean_setOptionFromString_match__1(lean_object*);
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__19;
 lean_object* l_Lean_Option_register(lean_object*);
 extern lean_object* l_termDepIfThenElse___closed__12;
 lean_object* l_Lean_Option_commandRegister__builtin__option_____x3a___x3a_x3d__;
@ -26,11 +27,13 @@ lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_OptionDecl_group___default;
 lean_object* l_Lean_Option_commandRegister__builtin__option_____x3a___x3a_x3d_____closed__11;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_2278____closed__2;
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__16;
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__2;
 lean_object* l_Std_RBNode_find___at_Lean_getOptionDecl___spec__1___boxed(lean_object*, lean_object*);
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__11;
 lean_object* l_Lean_KVMap_setNat(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Option_commandRegister__builtin__option_____x3a___x3a_x3d_____closed__3;
 extern lean_object* l_Array_empty___closed__1;
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__1;
 lean_object* l_Lean_Option_Decl_group___default;
 lean_object* lean_st_ref_get(lean_object*, lean_object*);
 extern lean_object* l_Lean_instInhabitedParserDescr___closed__1;
@ -38,14 +41,14 @@ lean_object* l_Lean_KVMap_setString(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_setOptionFromString_match__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_name_eq(lean_object*, lean_object*);
 lean_object* l_Lean_Option_get___rarg___boxed(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__7;
 lean_object* l_Lean_getOptionDefaulValue(lean_object*, lean_object*);
 lean_object* l_Lean_getOptionDecls(lean_object*);
+lean_object* l_Lean_Option_get_x3f(lean_object*);
 lean_object* l_Lean_instInhabitedOptionDecl___closed__1;
 lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* l_String_toInt_x3f(lean_object*);
 lean_object* lean_string_append(lean_object*, lean_object*);
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__11;
+lean_object* l_Lean_instForInOptionsProdNameDataValue___closed__1;
 lean_object* l_Lean_Option_commandRegister__builtin__option_____x3a___x3a_x3d_____closed__7;
 lean_object* l_Lean_KVMap_instToStringKVMap(lean_object*);
 lean_object* l_IO_mkRef___at___private_Lean_Data_Options_0__Lean_initOptionDeclsRef___spec__1(lean_object*, lean_object*);
@ -55,6 +58,7 @@ extern lean_object* l_instReprBool___closed__2;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_1481____closed__8;
 lean_object* l_Lean_getOptionDecl___closed__1;
 uint8_t l_Lean_NameMap_contains___rarg(lean_object*, lean_object*);
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__12;
 lean_object* l_Lean_setOptionFromString_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Name_toStringWithSep(lean_object*, lean_object*);
 lean_object* l_Lean_instInhabitedOptions;
@ -62,44 +66,43 @@ lean_object* l_Lean_setOptionFromString_match__4___rarg(lean_object*, lean_objec
 lean_object* l_Lean_getNatOption(lean_object*);
 lean_object* l_Lean_getBoolOption___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Option_get___rarg(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__1;
 lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_myMacro____x40_Init_Notation___hyg_113____spec__1(lean_object*, lean_object*);
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__7;
 lean_object* l_Lean_Option_setIfNotSet___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_registerOption___closed__1;
 lean_object* l_Lean_registerOption___closed__2;
 lean_object* l_Lean_Option_setIfNotSet(lean_object*);
 lean_object* l_Lean_Option_commandRegister__builtin__option_____x3a___x3a_x3d_____closed__5;
+lean_object* l_Lean_KVMap_instForInKVMapProdNameDataValue(lean_object*, lean_object*);
 lean_object* l___private_Lean_Data_Options_0__Lean_optionDeclsRef;
 lean_object* l_Lean_Option_commandRegister__builtin__option_____x3a___x3a_x3d_____closed__10;
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__12;
 lean_object* l_String_toName(lean_object*);
 lean_object* l_Lean_setOptionFromString___closed__4;
 lean_object* l_Lean_instMonadOptions(lean_object*, lean_object*);
 lean_object* l_Lean_getOptionDecl(lean_object*, lean_object*);
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__8;
 lean_object* l_Lean_OptionDecl_descr___default;
 lean_object* l_Lean_instToStringOptions;
 uint8_t l_Lean_KVMap_getBool(lean_object*, lean_object*, uint8_t);
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__19;
 lean_object* l_Lean_setOptionFromString_match__4(lean_object*);
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__16;
 lean_object* l_Lean_instMonadOptions___rarg(lean_object*, lean_object*);
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894_(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932_(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_instInhabitedDataValue___closed__1;
 uint8_t l_Lean_Name_quickCmp(lean_object*, lean_object*);
 lean_object* l_Std_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__2;
 lean_object* l_Lean_Option_commandRegister__builtin__option_____x3a___x3a_x3d_____closed__6;
 lean_object* lean_st_mk_ref(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getId(lean_object*);
 lean_object* lean_get_option_decls_array(lean_object*);
 lean_object* l_Lean_getNatOption___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_KVMap_setInt(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_instForInOptionsProdNameDataValue(lean_object*);
 uint8_t l_Lean_KVMap_contains(lean_object*, lean_object*);
 lean_object* l___private_Init_Meta_0__Lean_quoteName(lean_object*);
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__17;
 lean_object* l_Lean_Options_empty;
 extern lean_object* l_Array_forInUnsafe_loop___at___private_Init_NotationExtra_0__Lean_mkHintBody___spec__1___closed__3;
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__14;
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__3;
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__6;
 extern lean_object* l_Lean_Parser_Syntax_addPrec___closed__10;
 lean_object* l_Lean_setOptionFromString___closed__5;
 lean_object* l_Lean_Option_set___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -107,19 +110,23 @@ extern lean_object* l_termDepIfThenElse___closed__14;
 extern lean_object* l_termDepIfThenElse___closed__9;
 extern lean_object* l_termIfLet___x3a_x3d__Then__Else_____closed__8;
 lean_object* l_Lean_instInhabitedOptionDecl;
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__15;
 lean_object* l_Lean_getBoolOption___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__18;
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__10;
 lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_KVMap_getNat(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__20;
 lean_object* l_Lean_getOptionDecl_match__1___rarg(lean_object*, lean_object*, lean_object*);
 extern lean_object* l___private_Init_Meta_0__Lean_quoteOption___rarg___closed__1;
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__4;
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__9;
 extern lean_object* l_Lean_nullKind___closed__2;
 lean_object* l_Std_RBNode_fold___at_Lean_getOptionDeclsArray___spec__1(lean_object*, lean_object*);
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__14;
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__5;
 lean_object* l_Lean_KVMap_setName(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Option_register___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13;
 lean_object* l_Std_RBNode_find___at_Lean_getOptionDecl___spec__1(lean_object*, lean_object*);
+lean_object* l_Lean_Option_get_x3f___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_setOptionFromString(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_setOptionFromString___closed__6;
 lean_object* l_Lean_registerOption___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -129,13 +136,13 @@ extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1354____close
 lean_object* l_Lean_KVMap_insertCore(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_getBoolOption___rarg___lambda__1(lean_object*, lean_object*, uint8_t, lean_object*);
 lean_object* l_Lean_getNatOption___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Option_get_x3f___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* lean_register_option(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Option_commandRegister__builtin__option_____x3a___x3a_x3d_____closed__8;
 extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_23499____closed__8;
 lean_object* l_Lean_instInhabitedOption(lean_object*);
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_16268____closed__9;
 lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__10;
 lean_object* l_Lean_Option_Decl_descr___default;
 lean_object* l_Lean_getBoolOption(lean_object*);
 lean_object* l_Lean_KVMap_findCore(lean_object*, lean_object*);
@ -144,7 +151,6 @@ lean_object* l_Lean_Option_commandRegister__builtin__option_____x3a___x3a_x3d___
 lean_object* l_String_trim(lean_object*);
 lean_object* l_Lean_getOptionDecl_match__1(lean_object*);
 lean_object* l_Lean_setOptionFromString_match__2(lean_object*);
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__20;
 lean_object* l_Lean_Option_commandRegister__builtin__option_____x3a___x3a_x3d_____closed__9;
 uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
 lean_object* l_Lean_instToStringOptions___closed__1;
@ -152,6 +158,7 @@ lean_object* l_Lean_Option_commandRegister__builtin__option_____x3a___x3a_x3d___
 lean_object* l_Std_RBNode_fold___at_Lean_getOptionDeclsArray___spec__1___boxed(lean_object*, lean_object*);
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_2278____closed__4;
 lean_object* l_List_map___at_Lean_setOptionFromString___spec__1(lean_object*);
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13;
 lean_object* l___private_Lean_Data_Options_0__Lean_initOptionDeclsRef(lean_object*);
 lean_object* l_Lean_Option_get(lean_object*);
 lean_object* l_Lean_setOptionFromString___closed__2;
@ -159,20 +166,19 @@ lean_object* l_Lean_Option_commandRegister__builtin__option_____x3a___x3a_x3d___
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 lean_object* l_String_toNat_x3f(lean_object*);
 extern lean_object* l_Lean_expandExplicitBindersAux_loop___closed__4;
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__17;
 lean_object* l_Lean_registerOption___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__3;
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__8;
 extern lean_object* l_Lean_Parser_Tactic_rwRule___closed__3;
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__6;
 lean_object* l_Lean_setOptionFromString___closed__7;
 lean_object* l_Lean_instInhabitedOptionDecls;
 lean_object* l_Lean_setOptionFromString_match__2___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__4;
 lean_object* l_Lean_getOptionDescr(lean_object*, lean_object*);
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__18;
 lean_object* l_Lean_setOptionFromString___closed__3;
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__15;
 lean_object* l_Lean_getNatOption___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__5;
 lean_object* l_Lean_instInhabitedOption___rarg(lean_object*);
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__9;
 static lean_object* _init_l_Lean_Options_empty() {
 _start:
 {
@ -205,6 +211,23 @@ x_1 = l_Lean_instToStringOptions___closed__1;
 return x_1;
 }
 }
+static lean_object* _init_l_Lean_instForInOptionsProdNameDataValue___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_KVMap_instForInKVMapProdNameDataValue), 2, 1);
+lean_closure_set(x_1, 0, lean_box(0));
+return x_1;
+}
+}
+lean_object* l_Lean_instForInOptionsProdNameDataValue(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l_Lean_instForInOptionsProdNameDataValue___closed__1;
+return x_2;
+}
+}
 static lean_object* _init_l_Lean_OptionDecl_group___default() {
 _start:
 {
@ -1692,6 +1715,51 @@ x_1 = l_Lean_instInhabitedParserDescr___closed__1;
 return x_1;
 }
 }
+lean_object* l_Lean_Option_get_x3f___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; lean_object* x_5; 
+x_4 = lean_ctor_get(x_3, 0);
+x_5 = l_Lean_KVMap_findCore(x_2, x_4);
+if (lean_obj_tag(x_5) == 0)
+{
+lean_object* x_6; 
+lean_dec(x_1);
+x_6 = lean_box(0);
+return x_6;
+}
+else
+{
+lean_object* x_7; lean_object* x_8; lean_object* x_9; 
+x_7 = lean_ctor_get(x_5, 0);
+lean_inc(x_7);
+lean_dec(x_5);
+x_8 = lean_ctor_get(x_1, 1);
+lean_inc(x_8);
+lean_dec(x_1);
+x_9 = lean_apply_1(x_8, x_7);
+return x_9;
+}
+}
+}
+lean_object* l_Lean_Option_get_x3f(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_Option_get_x3f___rarg___boxed), 3, 0);
+return x_2;
+}
+}
+lean_object* l_Lean_Option_get_x3f___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Lean_Option_get_x3f___rarg(x_1, x_2, x_3);
+lean_dec(x_3);
+lean_dec(x_2);
+return x_4;
+}
+}
 lean_object* l_Lean_Option_get___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
@ -2027,7 +2095,7 @@ x_1 = l_Lean_Option_commandRegister__builtin__option_____x3a___x3a_x3d_____close
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__1() {
+static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__1() {
 _start:
 {
 lean_object* x_1; 
@ -2035,17 +2103,17 @@ x_1 = lean_mk_string("builtin_initialize");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__2() {
+static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1354____closed__3;
-x_2 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__1;
+x_2 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__3() {
+static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__3() {
 _start:
 {
 lean_object* x_1; 
@ -2053,22 +2121,22 @@ x_1 = lean_mk_string("Lean.Option");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__4() {
+static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__3;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__3;
 x_2 = lean_string_utf8_byte_size(x_1);
 return x_2;
 }
 }
-static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__5() {
+static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__3;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__3;
 x_2 = lean_unsigned_to_nat(0u);
-x_3 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__4;
+x_3 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__4;
 x_4 = lean_alloc_ctor(0, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);
@ -2076,7 +2144,7 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
-static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__6() {
+static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
@ -2088,19 +2156,19 @@ lean_ctor_set(x_3, 1, x_1);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__7() {
+static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__7() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__6;
+x_2 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__6;
 x_3 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_3, 0, x_2);
 lean_ctor_set(x_3, 1, x_1);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__8() {
+static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__8() {
 _start:
 {
 lean_object* x_1; 
@ -2108,17 +2176,17 @@ x_1 = lean_mk_string("doSeqIndent");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__9() {
+static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__9() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_myMacro____x40_Init_Notation___hyg_2278____closed__2;
-x_2 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__8;
+x_2 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__8;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__10() {
+static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__10() {
 _start:
 {
 lean_object* x_1; 
@ -2126,17 +2194,17 @@ x_1 = lean_mk_string("doSeqItem");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__11() {
+static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__11() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_myMacro____x40_Init_Notation___hyg_2278____closed__2;
-x_2 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__10;
+x_2 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__10;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__12() {
+static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__12() {
 _start:
 {
 lean_object* x_1; 
@ -2144,17 +2212,17 @@ x_1 = lean_mk_string("doExpr");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13() {
+static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_myMacro____x40_Init_Notation___hyg_2278____closed__2;
-x_2 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__12;
+x_2 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__12;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__14() {
+static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__14() {
 _start:
 {
 lean_object* x_1; 
@ -2162,22 +2230,22 @@ x_1 = lean_mk_string("Lean.Option.register");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__15() {
+static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__15() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__14;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__14;
 x_2 = lean_string_utf8_byte_size(x_1);
 return x_2;
 }
 }
-static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__16() {
+static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__16() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__14;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__14;
 x_2 = lean_unsigned_to_nat(0u);
-x_3 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__15;
+x_3 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__15;
 x_4 = lean_alloc_ctor(0, 3, 0);
 lean_ctor_set(x_4, 0, x_1);
 lean_ctor_set(x_4, 1, x_2);
@ -2185,7 +2253,7 @@ lean_ctor_set(x_4, 2, x_3);
 return x_4;
 }
 }
-static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__17() {
+static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__17() {
 _start:
 {
 lean_object* x_1; 
@ -2193,41 +2261,41 @@ x_1 = lean_mk_string("register");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__18() {
+static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__18() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Option_commandRegister__builtin__option_____x3a___x3a_x3d_____closed__1;
-x_2 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__17;
+x_2 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__17;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__19() {
+static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__19() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__18;
+x_2 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__18;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_2);
 lean_ctor_set(x_3, 1, x_1);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__20() {
+static lean_object* _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__20() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__19;
+x_2 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__19;
 x_3 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_3, 0, x_2);
 lean_ctor_set(x_3, 1, x_1);
 return x_3;
 }
 }
-lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 lean_object* x_4; uint8_t x_5; 
@ -2266,7 +2334,7 @@ lean_inc(x_17);
 x_18 = lean_ctor_get(x_2, 1);
 lean_inc(x_18);
 lean_dec(x_2);
-x_19 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__1;
+x_19 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__1;
 lean_inc(x_16);
 x_20 = lean_alloc_ctor(2, 2, 0);
 lean_ctor_set(x_20, 0, x_16);
@ -2285,8 +2353,8 @@ x_27 = l_Lean_Option_commandRegister__builtin__option_____x3a___x3a_x3d_____clos
 lean_inc(x_17);
 lean_inc(x_18);
 x_28 = l_Lean_addMacroScope(x_18, x_27, x_17);
-x_29 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__5;
-x_30 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__7;
+x_29 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__5;
+x_30 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__7;
 lean_inc(x_16);
 x_31 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_31, 0, x_16);
@ -2320,10 +2388,10 @@ x_46 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_46, 0, x_34);
 lean_ctor_set(x_46, 1, x_45);
 x_47 = lean_array_push(x_22, x_46);
-x_48 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__18;
+x_48 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__18;
 x_49 = l_Lean_addMacroScope(x_18, x_48, x_17);
-x_50 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__16;
-x_51 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__20;
+x_50 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__16;
+x_51 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__20;
 x_52 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_52, 0, x_16);
 lean_ctor_set(x_52, 1, x_50);
@ -2343,14 +2411,14 @@ x_60 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_60, 0, x_37);
 lean_ctor_set(x_60, 1, x_59);
 x_61 = lean_array_push(x_21, x_60);
-x_62 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13;
+x_62 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13;
 x_63 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_63, 0, x_62);
 lean_ctor_set(x_63, 1, x_61);
 x_64 = lean_array_push(x_21, x_63);
 x_65 = l_myMacro____x40_Init_Notation___hyg_1481____closed__8;
 x_66 = lean_array_push(x_64, x_65);
-x_67 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__11;
+x_67 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__11;
 x_68 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_68, 0, x_67);
 lean_ctor_set(x_68, 1, x_66);
@ -2359,12 +2427,12 @@ x_70 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_70, 0, x_34);
 lean_ctor_set(x_70, 1, x_69);
 x_71 = lean_array_push(x_21, x_70);
-x_72 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__9;
+x_72 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__9;
 x_73 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_73, 0, x_72);
 lean_ctor_set(x_73, 1, x_71);
 x_74 = lean_array_push(x_47, x_73);
-x_75 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__2;
+x_75 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__2;
 x_76 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_76, 0, x_75);
 lean_ctor_set(x_76, 1, x_74);
@ -2384,7 +2452,7 @@ lean_inc(x_79);
 x_80 = lean_ctor_get(x_2, 1);
 lean_inc(x_80);
 lean_dec(x_2);
-x_81 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__1;
+x_81 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__1;
 lean_inc(x_77);
 x_82 = lean_alloc_ctor(2, 2, 0);
 lean_ctor_set(x_82, 0, x_77);
@ -2403,8 +2471,8 @@ x_89 = l_Lean_Option_commandRegister__builtin__option_____x3a___x3a_x3d_____clos
 lean_inc(x_79);
 lean_inc(x_80);
 x_90 = l_Lean_addMacroScope(x_80, x_89, x_79);
-x_91 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__5;
-x_92 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__7;
+x_91 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__5;
+x_92 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__7;
 lean_inc(x_77);
 x_93 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_93, 0, x_77);
@ -2438,10 +2506,10 @@ x_108 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_108, 0, x_96);
 lean_ctor_set(x_108, 1, x_107);
 x_109 = lean_array_push(x_84, x_108);
-x_110 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__18;
+x_110 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__18;
 x_111 = l_Lean_addMacroScope(x_80, x_110, x_79);
-x_112 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__16;
-x_113 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__20;
+x_112 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__16;
+x_113 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__20;
 x_114 = lean_alloc_ctor(3, 4, 0);
 lean_ctor_set(x_114, 0, x_77);
 lean_ctor_set(x_114, 1, x_112);
@ -2461,14 +2529,14 @@ x_122 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_122, 0, x_99);
 lean_ctor_set(x_122, 1, x_121);
 x_123 = lean_array_push(x_83, x_122);
-x_124 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13;
+x_124 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13;
 x_125 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_125, 0, x_124);
 lean_ctor_set(x_125, 1, x_123);
 x_126 = lean_array_push(x_83, x_125);
 x_127 = l_myMacro____x40_Init_Notation___hyg_1481____closed__8;
 x_128 = lean_array_push(x_126, x_127);
-x_129 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__11;
+x_129 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__11;
 x_130 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_130, 0, x_129);
 lean_ctor_set(x_130, 1, x_128);
@ -2477,12 +2545,12 @@ x_132 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_132, 0, x_96);
 lean_ctor_set(x_132, 1, x_131);
 x_133 = lean_array_push(x_83, x_132);
-x_134 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__9;
+x_134 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__9;
 x_135 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_135, 0, x_134);
 lean_ctor_set(x_135, 1, x_133);
 x_136 = lean_array_push(x_109, x_135);
-x_137 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__2;
+x_137 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__2;
 x_138 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_138, 0, x_137);
 lean_ctor_set(x_138, 1, x_136);
@ -2515,6 +2583,8 @@ l_Lean_instToStringOptions___closed__1 = _init_l_Lean_instToStringOptions___clos
 lean_mark_persistent(l_Lean_instToStringOptions___closed__1);
 l_Lean_instToStringOptions = _init_l_Lean_instToStringOptions();
 lean_mark_persistent(l_Lean_instToStringOptions);
+l_Lean_instForInOptionsProdNameDataValue___closed__1 = _init_l_Lean_instForInOptionsProdNameDataValue___closed__1();
+lean_mark_persistent(l_Lean_instForInOptionsProdNameDataValue___closed__1);
 l_Lean_OptionDecl_group___default = _init_l_Lean_OptionDecl_group___default();
 lean_mark_persistent(l_Lean_OptionDecl_group___default);
 l_Lean_OptionDecl_descr___default = _init_l_Lean_OptionDecl_descr___default();
@ -2578,46 +2648,46 @@ l_Lean_Option_commandRegister__builtin__option_____x3a___x3a_x3d_____closed__11
 lean_mark_persistent(l_Lean_Option_commandRegister__builtin__option_____x3a___x3a_x3d_____closed__11);
 l_Lean_Option_commandRegister__builtin__option_____x3a___x3a_x3d__ = _init_l_Lean_Option_commandRegister__builtin__option_____x3a___x3a_x3d__();
 lean_mark_persistent(l_Lean_Option_commandRegister__builtin__option_____x3a___x3a_x3d__);
-l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__1 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__1();
-lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__1);
-l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__2 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__2();
-lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__2);
-l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__3 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__3();
-lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__3);
-l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__4 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__4();
-lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__4);
-l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__5 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__5();
-lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__5);
-l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__6 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__6();
-lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__6);
-l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__7 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__7();
-lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__7);
-l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__8 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__8();
-lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__8);
-l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__9 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__9();
-lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__9);
-l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__10 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__10();
-lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__10);
-l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__11 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__11();
-lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__11);
-l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__12 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__12();
-lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__12);
-l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13();
-lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13);
-l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__14 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__14();
-lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__14);
-l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__15 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__15();
-lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__15);
-l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__16 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__16();
-lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__16);
-l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__17 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__17();
-lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__17);
-l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__18 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__18();
-lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__18);
-l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__19 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__19();
-lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__19);
-l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__20 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__20();
-lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__20);
+l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__1 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__1();
+lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__1);
+l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__2 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__2();
+lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__2);
+l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__3 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__3();
+lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__3);
+l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__4 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__4();
+lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__4);
+l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__5 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__5();
+lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__5);
+l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__6 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__6();
+lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__6);
+l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__7 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__7();
+lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__7);
+l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__8 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__8();
+lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__8);
+l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__9 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__9();
+lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__9);
+l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__10 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__10();
+lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__10);
+l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__11 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__11();
+lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__11);
+l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__12 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__12();
+lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__12);
+l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13();
+lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13);
+l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__14 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__14();
+lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__14);
+l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__15 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__15();
+lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__15);
+l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__16 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__16();
+lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__16);
+l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__17 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__17();
+lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__17);
+l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__18 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__18();
+lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__18);
+l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__19 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__19();
+lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__19);
+l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__20 = _init_l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__20();
+lean_mark_persistent(l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__20);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus
--- a/stage0/stdlib/Lean/Elab.c
+++ b/stage0/stdlib/Lean/Elab.c
@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Lean.Elab
-// Imports: Init Lean.Elab.Import Lean.Elab.Exception Lean.Elab.Command Lean.Elab.Term Lean.Elab.App Lean.Elab.Binders Lean.Elab.LetRec Lean.Elab.Frontend Lean.Elab.BuiltinNotation Lean.Elab.Declaration Lean.Elab.Tactic Lean.Elab.Match Lean.Elab.Quotation Lean.Elab.Syntax Lean.Elab.Do Lean.Elab.StructInst Lean.Elab.Inductive Lean.Elab.Structure Lean.Elab.Print Lean.Elab.MutualDef Lean.Elab.PreDefinition Lean.Elab.Deriving Lean.Elab.DeclarationRange Lean.Elab.Extra
+// Imports: Init Lean.Elab.Import Lean.Elab.Exception Lean.Elab.Command Lean.Elab.Term Lean.Elab.App Lean.Elab.Binders Lean.Elab.LetRec Lean.Elab.Frontend Lean.Elab.BuiltinNotation Lean.Elab.Declaration Lean.Elab.Tactic Lean.Elab.Match Lean.Elab.Quotation Lean.Elab.Syntax Lean.Elab.Do Lean.Elab.StructInst Lean.Elab.Inductive Lean.Elab.Structure Lean.Elab.Print Lean.Elab.MutualDef Lean.Elab.PreDefinition Lean.Elab.Deriving Lean.Elab.DeclarationRange Lean.Elab.Extra Lean.Elab.GenInjective
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@ -38,6 +38,7 @@ lean_object* initialize_Lean_Elab_PreDefinition(lean_object*);
 lean_object* initialize_Lean_Elab_Deriving(lean_object*);
 lean_object* initialize_Lean_Elab_DeclarationRange(lean_object*);
 lean_object* initialize_Lean_Elab_Extra(lean_object*);
+lean_object* initialize_Lean_Elab_GenInjective(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Lean_Elab(lean_object* w) {
 lean_object * res;
@ -118,6 +119,9 @@ lean_dec_ref(res);
 res = initialize_Lean_Elab_Extra(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Lean_Elab_GenInjective(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus
--- a/stage0/stdlib/Lean/Elab/Declaration.c
+++ b/stage0/stdlib/Lean/Elab/Declaration.c
@ -53,6 +53,7 @@ lean_object* l_Array_append___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_getDeclarationRange___at_Lean_Elab_Command_elabAxiom___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Elab_Modifiers_isProtected(lean_object*);
 lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__3___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__2;
 extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1354____closed__12;
 lean_object* l___regBuiltin_Lean_Elab_Command_expandInitialize___closed__1;
 lean_object* l_Lean_Elab_Command_checkValidCtorModifier___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -163,7 +164,6 @@ lean_object* l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__21(lea
 extern lean_object* l_Lean_Parser_Command_namespace___elambda__1___closed__2;
 lean_object* l___regBuiltin_Lean_Elab_Command_expandMutualPreamble(lean_object*);
 lean_object* l_Lean_Elab_Command_expandInitCmd___closed__10;
-extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__2;
 lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabAttr___spec__2(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_609____closed__2;
 lean_object* l_Lean_Elab_Command_expandDeclNamespace_x3f_match__1(lean_object*);
@ -8175,7 +8175,7 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_2 = l_Lean_Elab_macroAttribute;
-x_3 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__2;
+x_3 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__2;
 x_4 = l___regBuiltin_Lean_Elab_Command_expandBuiltinInitialize___closed__1;
 x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
--- a/stage0/stdlib/Lean/Elab/Deriving/FromToJson.c
+++ b/stage0/stdlib/Lean/Elab/Deriving/FromToJson.c
@ -37,6 +37,7 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_2278____closed__2;
 lean_object* l_Array_append___rarg(lean_object*, lean_object*);
 lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
 lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler___lambda__1___closed__23;
+extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__11;
 extern lean_object* l_Lean_Parser_Term_tupleTail___elambda__1___closed__1;
 lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler___lambda__1___closed__21;
 lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -53,7 +54,6 @@ lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler(lean_obje
 lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___lambda__1___closed__6;
 lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
-extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__11;
 lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler_match__1___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler___lambda__1___closed__6;
@ -64,6 +64,7 @@ lean_object* l_Lean_Elab_Term_getMainModule___rarg(lean_object*, lean_object*);
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_1481____closed__8;
 uint8_t l_USize_decLt(size_t, size_t);
 lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler___lambda__1___closed__25;
+extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__12;
 lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___lambda__1___closed__1;
 lean_object* l_Lean_Elab_Deriving_FromToJson_initFn____x40_Lean_Elab_Deriving_FromToJson___hyg_1633____closed__2;
 lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler(lean_object*, lean_object*, lean_object*, lean_object*);
@ -85,7 +86,6 @@ lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_FromToJson_mkToJsonI
 lean_object* l_Lean_Elab_Deriving_FromToJson_mkJsonField___lambda__1___boxed(lean_object*);
 lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler___lambda__1___closed__3;
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
-extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__12;
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_16821____closed__11;
 extern lean_object* l_term___x3c_x7c_____closed__2;
 extern lean_object* l_myMacro____x40_Init_NotationExtra___hyg_5711____closed__3;
@ -121,12 +121,12 @@ lean_object* l_Lean_Elab_Deriving_mkHeader___rarg(lean_object*, lean_object*, le
 lean_object* l_ReaderT_bind___at_Lean_Elab_Term_instMonadLogTermElabM___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___lambda__1___closed__12;
 size_t lean_usize_of_nat(lean_object*);
+extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__10;
 extern lean_object* l_term_x7b_x7d___closed__5;
 lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_doReturn___elambda__1___closed__2;
 lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___spec__1___closed__4;
 extern lean_object* l___private_Init_Meta_0__Lean_quoteOption___rarg___closed__1;
-extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__9;
 lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_nullKind___closed__2;
 lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler_match__1(lean_object*);
@ -152,7 +152,6 @@ lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler___lambda_
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_16268____closed__9;
 lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler___lambda__1___closed__2;
 extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_369____closed__3;
-extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__10;
 extern lean_object* l_Lean_instInhabitedName;
 lean_object* l_Lean_Elab_Deriving_FromToJson_initFn____x40_Lean_Elab_Deriving_FromToJson___hyg_1633____closed__1;
 lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -198,6 +197,7 @@ extern lean_object* l_term_x5b___x5d___closed__3;
 lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler___lambda__1___closed__4;
 uint8_t lean_string_dec_eq(lean_object*, lean_object*);
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
+extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__9;
 uint8_t l_Lean_Elab_Deriving_FromToJson_mkJsonField___lambda__1(uint32_t x_1) {
 _start:
 {
@ -2060,7 +2060,7 @@ if (x_24 == 0)
 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; 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; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; 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; 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; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; 
 x_25 = lean_ctor_get(x_21, 0);
 x_26 = lean_ctor_get(x_21, 1);
-x_27 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__10;
+x_27 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__10;
 lean_inc(x_7);
 x_28 = lean_name_mk_string(x_7, x_27);
 x_29 = l_Lean_Parser_Term_doLetArrow___elambda__1___closed__1;
@ -2088,7 +2088,7 @@ x_40 = lean_alloc_ctor(2, 2, 0);
 lean_ctor_set(x_40, 0, x_1);
 lean_ctor_set(x_40, 1, x_39);
 x_41 = lean_array_push(x_38, x_40);
-x_42 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__12;
+x_42 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__12;
 lean_inc(x_7);
 x_43 = lean_name_mk_string(x_7, x_42);
 x_44 = l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler___spec__2___closed__4;
@ -2173,7 +2173,7 @@ x_76 = lean_ctor_get(x_21, 1);
 lean_inc(x_76);
 lean_inc(x_75);
 lean_dec(x_21);
-x_77 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__10;
+x_77 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__10;
 lean_inc(x_7);
 x_78 = lean_name_mk_string(x_7, x_77);
 x_79 = l_Lean_Parser_Term_doLetArrow___elambda__1___closed__1;
@ -2201,7 +2201,7 @@ x_90 = lean_alloc_ctor(2, 2, 0);
 lean_ctor_set(x_90, 0, x_1);
 lean_ctor_set(x_90, 1, x_89);
 x_91 = lean_array_push(x_88, x_90);
-x_92 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__12;
+x_92 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__12;
 lean_inc(x_7);
 x_93 = lean_name_mk_string(x_7, x_92);
 x_94 = l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler___spec__2___closed__4;
@ -2925,7 +2925,7 @@ lean_ctor_set(x_178, 0, x_177);
 lean_ctor_set(x_178, 1, x_176);
 x_179 = lean_array_push(x_48, x_178);
 x_180 = lean_array_push(x_179, x_57);
-x_181 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__11;
+x_181 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__11;
 x_182 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_182, 0, x_181);
 lean_ctor_set(x_182, 1, x_180);
@ -2934,7 +2934,7 @@ x_184 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_184, 0, x_53);
 lean_ctor_set(x_184, 1, x_183);
 x_185 = lean_array_push(x_48, x_184);
-x_186 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__9;
+x_186 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__9;
 x_187 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_187, 0, x_186);
 lean_ctor_set(x_187, 1, x_185);
--- a/stage0/stdlib/Lean/Elab/Do.c
+++ b/stage0/stdlib/Lean/Elab/Do.c
--- a/stage0/stdlib/Lean/Elab/GenInjective.c
+++ b/stage0/stdlib/Lean/Elab/GenInjective.c
@ -0,0 +1,473 @@
+// Lean compiler output
+// Module: Lean.Elab.GenInjective
+// Imports: Init Lean.Elab.Command Lean.Meta.Injective
+#include <lean/lean.h>
+#if defined(__clang__)
+#pragma clang diagnostic ignored "-Wunused-parameter"
+#pragma clang diagnostic ignored "-Wunused-label"
+#elif defined(__GNUC__) && !defined(__CLANG__)
+#pragma GCC diagnostic ignored "-Wunused-parameter"
+#pragma GCC diagnostic ignored "-Wunused-label"
+#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
+#endif
+#ifdef __cplusplus
+extern "C" {
+#endif
+lean_object* l_Lean_Elab_Command_elabGenInjectiveTheorems___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Command_liftTermElabM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_List_toString___at_Lean_resolveGlobalConstNoOverload___spec__2(lean_object*);
+extern lean_object* l_Lean_Elab_Command_commandElabAttribute;
+lean_object* l_Lean_Elab_Command_elabGenInjectiveTheorems___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_mkInjectiveTheorems(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* lean_st_ref_get(lean_object*, lean_object*);
+extern lean_object* l_Lean_instInhabitedParserDescr___closed__1;
+lean_object* lean_string_append(lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Command_elabGenInjectiveTheorems___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_resolveGlobalName___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_throwUnknownConstant___rarg___closed__2;
+lean_object* l_List_map___at_Lean_resolveGlobalConstNoOverload___spec__1(lean_object*, lean_object*);
+lean_object* l_Lean_resolveGlobalConst___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__21(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l___regBuiltin_Lean_Elab_Command_elabGenInjectiveTheorems___closed__1;
+lean_object* l_Lean_Syntax_getId(lean_object*);
+lean_object* l_Lean_throwError___at_Lean_Elab_Command_elabExport___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_List_filterAux___at_Lean_resolveGlobalConst___spec__1(lean_object*, lean_object*);
+lean_object* lean_expr_dbg_to_string(lean_object*);
+extern lean_object* l_Lean_Parser_Command_genInjectiveTheorems___elambda__1___closed__2;
+lean_object* l_Lean_ResolveName_resolveGlobalName(lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_KernelException_toMessageData___closed__3;
+extern lean_object* l_Lean_resolveGlobalConstNoOverload___rarg___lambda__1___closed__1;
+extern lean_object* l_Lean_resolveGlobalConstNoOverload___rarg___lambda__1___closed__2;
+lean_object* l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_resolveGlobalConst___at_Lean_registerInitAttrUnsafe___spec__4___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_resolveGlobalConst___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
+lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
+uint8_t l_List_isEmpty___rarg(lean_object*);
+lean_object* l_Lean_Elab_Command_getScope___rarg(lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Command_elabGenInjectiveTheorems(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_mkConst(lean_object*, lean_object*);
+lean_object* l_Lean_resolveGlobalName___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l___regBuiltin_Lean_Elab_Command_elabGenInjectiveTheorems(lean_object*);
+lean_object* l_Lean_resolveGlobalName___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14; 
+x_5 = lean_st_ref_get(x_3, x_4);
+x_6 = lean_ctor_get(x_5, 0);
+lean_inc(x_6);
+x_7 = lean_ctor_get(x_5, 1);
+lean_inc(x_7);
+lean_dec(x_5);
+x_8 = lean_ctor_get(x_6, 0);
+lean_inc(x_8);
+lean_dec(x_6);
+x_9 = l_Lean_Elab_Command_getScope___rarg(x_3, x_7);
+x_10 = lean_ctor_get(x_9, 0);
+lean_inc(x_10);
+x_11 = lean_ctor_get(x_9, 1);
+lean_inc(x_11);
+lean_dec(x_9);
+x_12 = lean_ctor_get(x_10, 2);
+lean_inc(x_12);
+lean_dec(x_10);
+x_13 = l_Lean_Elab_Command_getScope___rarg(x_3, x_11);
+x_14 = !lean_is_exclusive(x_13);
+if (x_14 == 0)
+{
+lean_object* x_15; lean_object* x_16; lean_object* x_17; 
+x_15 = lean_ctor_get(x_13, 0);
+x_16 = lean_ctor_get(x_15, 3);
+lean_inc(x_16);
+lean_dec(x_15);
+x_17 = l_Lean_ResolveName_resolveGlobalName(x_8, x_12, x_16, x_1);
+lean_dec(x_12);
+lean_ctor_set(x_13, 0, x_17);
+return x_13;
+}
+else
+{
+lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; 
+x_18 = lean_ctor_get(x_13, 0);
+x_19 = lean_ctor_get(x_13, 1);
+lean_inc(x_19);
+lean_inc(x_18);
+lean_dec(x_13);
+x_20 = lean_ctor_get(x_18, 3);
+lean_inc(x_20);
+lean_dec(x_18);
+x_21 = l_Lean_ResolveName_resolveGlobalName(x_8, x_12, x_20, x_1);
+lean_dec(x_12);
+x_22 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_22, 0, x_21);
+lean_ctor_set(x_22, 1, x_19);
+return x_22;
+}
+}
+}
+lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+x_5 = lean_box(0);
+x_6 = l_Lean_mkConst(x_1, x_5);
+x_7 = lean_alloc_ctor(2, 1, 0);
+lean_ctor_set(x_7, 0, x_6);
+x_8 = l_Lean_throwUnknownConstant___rarg___closed__2;
+x_9 = lean_alloc_ctor(10, 2, 0);
+lean_ctor_set(x_9, 0, x_8);
+lean_ctor_set(x_9, 1, x_7);
+x_10 = l_Lean_KernelException_toMessageData___closed__3;
+x_11 = lean_alloc_ctor(10, 2, 0);
+lean_ctor_set(x_11, 0, x_9);
+lean_ctor_set(x_11, 1, x_10);
+x_12 = l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__21(x_11, x_2, x_3, x_4);
+return x_12;
+}
+}
+lean_object* l_Lean_resolveGlobalConst___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; 
+lean_inc(x_1);
+x_5 = l_Lean_resolveGlobalName___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__3(x_1, x_2, x_3, x_4);
+x_6 = lean_ctor_get(x_5, 0);
+lean_inc(x_6);
+x_7 = lean_ctor_get(x_5, 1);
+lean_inc(x_7);
+lean_dec(x_5);
+x_8 = lean_box(0);
+x_9 = l_List_filterAux___at_Lean_resolveGlobalConst___spec__1(x_6, x_8);
+x_10 = l_List_isEmpty___rarg(x_9);
+if (x_10 == 0)
+{
+lean_object* x_11; lean_object* x_12; 
+lean_dec(x_1);
+x_11 = lean_box(0);
+x_12 = l_Lean_resolveGlobalConst___at_Lean_registerInitAttrUnsafe___spec__4___lambda__1(x_9, x_11, x_2, x_3, x_7);
+lean_dec(x_2);
+return x_12;
+}
+else
+{
+lean_object* x_13; uint8_t x_14; 
+lean_dec(x_9);
+x_13 = l_Lean_throwUnknownConstant___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__4(x_1, x_2, x_3, x_7);
+x_14 = !lean_is_exclusive(x_13);
+if (x_14 == 0)
+{
+return x_13;
+}
+else
+{
+lean_object* x_15; lean_object* x_16; lean_object* x_17; 
+x_15 = lean_ctor_get(x_13, 0);
+x_16 = lean_ctor_get(x_13, 1);
+lean_inc(x_16);
+lean_inc(x_15);
+lean_dec(x_13);
+x_17 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_17, 0, x_15);
+lean_ctor_set(x_17, 1, x_16);
+return x_17;
+}
+}
+}
+}
+lean_object* l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+lean_inc(x_2);
+lean_inc(x_1);
+x_5 = l_Lean_resolveGlobalConst___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__2(x_1, x_2, x_3, x_4);
+if (lean_obj_tag(x_5) == 0)
+{
+lean_object* x_6; 
+x_6 = lean_ctor_get(x_5, 0);
+lean_inc(x_6);
+if (lean_obj_tag(x_6) == 0)
+{
+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; lean_object* x_22; 
+x_7 = lean_ctor_get(x_5, 1);
+lean_inc(x_7);
+lean_dec(x_5);
+x_8 = lean_box(0);
+x_9 = l_Lean_mkConst(x_1, x_8);
+x_10 = lean_expr_dbg_to_string(x_9);
+lean_dec(x_9);
+x_11 = l_Lean_resolveGlobalConstNoOverload___rarg___lambda__1___closed__1;
+x_12 = lean_string_append(x_11, x_10);
+lean_dec(x_10);
+x_13 = l_Lean_resolveGlobalConstNoOverload___rarg___lambda__1___closed__2;
+x_14 = lean_string_append(x_12, x_13);
+x_15 = l_List_map___at_Lean_resolveGlobalConstNoOverload___spec__1(x_8, x_6);
+x_16 = l_List_toString___at_Lean_resolveGlobalConstNoOverload___spec__2(x_15);
+x_17 = lean_string_append(x_14, x_16);
+lean_dec(x_16);
+x_18 = l_Lean_instInhabitedParserDescr___closed__1;
+x_19 = lean_string_append(x_17, x_18);
+x_20 = lean_alloc_ctor(2, 1, 0);
+lean_ctor_set(x_20, 0, x_19);
+x_21 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_21, 0, x_20);
+x_22 = l_Lean_throwError___at_Lean_Elab_Command_elabExport___spec__2(x_21, x_2, x_3, x_7);
+return x_22;
+}
+else
+{
+lean_object* x_23; 
+x_23 = lean_ctor_get(x_6, 1);
+lean_inc(x_23);
+if (lean_obj_tag(x_23) == 0)
+{
+uint8_t x_24; 
+lean_dec(x_2);
+lean_dec(x_1);
+x_24 = !lean_is_exclusive(x_5);
+if (x_24 == 0)
+{
+lean_object* x_25; lean_object* x_26; 
+x_25 = lean_ctor_get(x_5, 0);
+lean_dec(x_25);
+x_26 = lean_ctor_get(x_6, 0);
+lean_inc(x_26);
+lean_dec(x_6);
+lean_ctor_set(x_5, 0, x_26);
+return x_5;
+}
+else
+{
+lean_object* x_27; lean_object* x_28; lean_object* x_29; 
+x_27 = lean_ctor_get(x_5, 1);
+lean_inc(x_27);
+lean_dec(x_5);
+x_28 = lean_ctor_get(x_6, 0);
+lean_inc(x_28);
+lean_dec(x_6);
+x_29 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_29, 0, x_28);
+lean_ctor_set(x_29, 1, x_27);
+return x_29;
+}
+}
+else
+{
+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; lean_object* x_43; lean_object* x_44; lean_object* x_45; 
+lean_dec(x_23);
+x_30 = lean_ctor_get(x_5, 1);
+lean_inc(x_30);
+lean_dec(x_5);
+x_31 = lean_box(0);
+x_32 = l_Lean_mkConst(x_1, x_31);
+x_33 = lean_expr_dbg_to_string(x_32);
+lean_dec(x_32);
+x_34 = l_Lean_resolveGlobalConstNoOverload___rarg___lambda__1___closed__1;
+x_35 = lean_string_append(x_34, x_33);
+lean_dec(x_33);
+x_36 = l_Lean_resolveGlobalConstNoOverload___rarg___lambda__1___closed__2;
+x_37 = lean_string_append(x_35, x_36);
+x_38 = l_List_map___at_Lean_resolveGlobalConstNoOverload___spec__1(x_31, x_6);
+x_39 = l_List_toString___at_Lean_resolveGlobalConstNoOverload___spec__2(x_38);
+x_40 = lean_string_append(x_37, x_39);
+lean_dec(x_39);
+x_41 = l_Lean_instInhabitedParserDescr___closed__1;
+x_42 = lean_string_append(x_40, x_41);
+x_43 = lean_alloc_ctor(2, 1, 0);
+lean_ctor_set(x_43, 0, x_42);
+x_44 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_44, 0, x_43);
+x_45 = l_Lean_throwError___at_Lean_Elab_Command_elabExport___spec__2(x_44, x_2, x_3, x_30);
+return x_45;
+}
+}
+}
+else
+{
+uint8_t x_46; 
+lean_dec(x_2);
+lean_dec(x_1);
+x_46 = !lean_is_exclusive(x_5);
+if (x_46 == 0)
+{
+return x_5;
+}
+else
+{
+lean_object* x_47; lean_object* x_48; lean_object* x_49; 
+x_47 = lean_ctor_get(x_5, 0);
+x_48 = lean_ctor_get(x_5, 1);
+lean_inc(x_48);
+lean_inc(x_47);
+lean_dec(x_5);
+x_49 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_49, 0, x_47);
+lean_ctor_set(x_49, 1, x_48);
+return x_49;
+}
+}
+}
+}
+lean_object* l_Lean_Elab_Command_elabGenInjectiveTheorems___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, lean_object* x_8) {
+_start:
+{
+lean_object* x_9; 
+x_9 = l_Lean_Meta_mkInjectiveTheorems(x_1, x_4, x_5, x_6, x_7, x_8);
+return x_9;
+}
+}
+lean_object* l_Lean_Elab_Command_elabGenInjectiveTheorems(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; 
+x_5 = lean_unsigned_to_nat(1u);
+x_6 = l_Lean_Syntax_getArg(x_1, x_5);
+x_7 = l_Lean_Syntax_getId(x_6);
+lean_dec(x_6);
+lean_inc(x_2);
+x_8 = l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__1(x_7, x_2, x_3, x_4);
+if (lean_obj_tag(x_8) == 0)
+{
+lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; 
+x_9 = lean_ctor_get(x_8, 0);
+lean_inc(x_9);
+x_10 = lean_ctor_get(x_8, 1);
+lean_inc(x_10);
+lean_dec(x_8);
+x_11 = lean_box(0);
+x_12 = lean_alloc_closure((void*)(l_Lean_Elab_Command_elabGenInjectiveTheorems___lambda__1___boxed), 8, 1);
+lean_closure_set(x_12, 0, x_9);
+x_13 = l_Lean_Elab_Command_liftTermElabM___rarg(x_11, x_12, x_2, x_3, x_10);
+return x_13;
+}
+else
+{
+uint8_t x_14; 
+lean_dec(x_2);
+x_14 = !lean_is_exclusive(x_8);
+if (x_14 == 0)
+{
+return x_8;
+}
+else
+{
+lean_object* x_15; lean_object* x_16; lean_object* x_17; 
+x_15 = lean_ctor_get(x_8, 0);
+x_16 = lean_ctor_get(x_8, 1);
+lean_inc(x_16);
+lean_inc(x_15);
+lean_dec(x_8);
+x_17 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_17, 0, x_15);
+lean_ctor_set(x_17, 1, x_16);
+return x_17;
+}
+}
+}
+}
+lean_object* l_Lean_resolveGlobalName___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+x_5 = l_Lean_resolveGlobalName___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__3(x_1, x_2, x_3, x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+return x_5;
+}
+}
+lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+x_5 = l_Lean_throwUnknownConstant___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__4(x_1, x_2, x_3, x_4);
+lean_dec(x_3);
+return x_5;
+}
+}
+lean_object* l_Lean_resolveGlobalConst___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+x_5 = l_Lean_resolveGlobalConst___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__2(x_1, x_2, x_3, x_4);
+lean_dec(x_3);
+return x_5;
+}
+}
+lean_object* l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+x_5 = l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__1(x_1, x_2, x_3, x_4);
+lean_dec(x_3);
+return x_5;
+}
+}
+lean_object* l_Lean_Elab_Command_elabGenInjectiveTheorems___lambda__1___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:
+{
+lean_object* x_9; 
+x_9 = l_Lean_Elab_Command_elabGenInjectiveTheorems___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
+lean_dec(x_3);
+lean_dec(x_2);
+return x_9;
+}
+}
+lean_object* l_Lean_Elab_Command_elabGenInjectiveTheorems___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+x_5 = l_Lean_Elab_Command_elabGenInjectiveTheorems(x_1, x_2, x_3, x_4);
+lean_dec(x_3);
+lean_dec(x_1);
+return x_5;
+}
+}
+static lean_object* _init_l___regBuiltin_Lean_Elab_Command_elabGenInjectiveTheorems___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Command_elabGenInjectiveTheorems___boxed), 4, 0);
+return x_1;
+}
+}
+lean_object* l___regBuiltin_Lean_Elab_Command_elabGenInjectiveTheorems(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_2 = l_Lean_Elab_Command_commandElabAttribute;
+x_3 = l_Lean_Parser_Command_genInjectiveTheorems___elambda__1___closed__2;
+x_4 = l___regBuiltin_Lean_Elab_Command_elabGenInjectiveTheorems___closed__1;
+x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
+return x_5;
+}
+}
+lean_object* initialize_Init(lean_object*);
+lean_object* initialize_Lean_Elab_Command(lean_object*);
+lean_object* initialize_Lean_Meta_Injective(lean_object*);
+static bool _G_initialized = false;
+lean_object* initialize_Lean_Elab_GenInjective(lean_object* w) {
+lean_object * res;
+if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
+_G_initialized = true;
+res = initialize_Init(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Elab_Command(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+res = initialize_Lean_Meta_Injective(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+l___regBuiltin_Lean_Elab_Command_elabGenInjectiveTheorems___closed__1 = _init_l___regBuiltin_Lean_Elab_Command_elabGenInjectiveTheorems___closed__1();
+lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabGenInjectiveTheorems___closed__1);
+res = l___regBuiltin_Lean_Elab_Command_elabGenInjectiveTheorems(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
+return lean_io_result_mk_ok(lean_box(0));
+}
+#ifdef __cplusplus
+}
+#endif
--- a/stage0/stdlib/Lean/Elab/Inductive.c
+++ b/stage0/stdlib/Lean/Elab/Inductive.c
--- a/stage0/stdlib/Lean/Elab/Structure.c
+++ b/stage0/stdlib/Lean/Elab/Structure.c
@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Lean.Elab.Structure
-// Imports: Init Lean.Parser.Command Lean.Meta.Closure Lean.Meta.SizeOf Lean.Elab.Command Lean.Elab.DeclModifiers Lean.Elab.DeclUtil Lean.Elab.Inductive Lean.Elab.DeclarationRange
+// Imports: Init Lean.Parser.Command Lean.Meta.Closure Lean.Meta.SizeOf Lean.Meta.Injective Lean.Elab.Command Lean.Elab.DeclModifiers Lean.Elab.DeclUtil Lean.Elab.Inductive Lean.Elab.DeclarationRange
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@ -101,6 +101,7 @@ lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lea
 lean_object* l_Lean_Elab_Command_checkValidFieldModifier___lambda__2___closed__1;
 lean_object* l_Lean_Elab_Command_checkValidFieldModifier___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_addDeclarationRanges___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__21___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_mkInjectiveTheorems(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_st_ref_get(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_checkValidFieldModifier___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withParents___rarg___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -544,7 +545,7 @@ lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields___r
 extern lean_object* l_Lean_Elab_Command_checkValidCtorModifier___rarg___lambda__2___closed__2;
 lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabStructure___spec__11(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__16___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_4848_(lean_object*);
+lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_4860_(lean_object*);
 lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__1___closed__1;
 uint8_t l___private_Lean_Expr_0__Lean_beqBinderInfo____x40_Lean_Expr___hyg_221_(uint8_t, uint8_t);
@ -9922,7 +9923,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___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields___rarg___closed__9;
 x_2 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields___rarg___closed__10;
-x_3 = lean_unsigned_to_nat(326u);
+x_3 = lean_unsigned_to_nat(327u);
 x_4 = lean_unsigned_to_nat(37u);
 x_5 = l_Lean_Name_getString_x21___closed__3;
 x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -18579,116 +18580,156 @@ lean_object* x_32; lean_object* x_33;
 x_32 = lean_ctor_get(x_31, 1);
 lean_inc(x_32);
 lean_dec(x_31);
+lean_inc(x_18);
+lean_inc(x_17);
+lean_inc(x_16);
+lean_inc(x_15);
 lean_inc(x_5);
 x_33 = l_Lean_Meta_mkSizeOfInstances(x_5, x_15, x_16, x_17, x_18, x_32);
 if (lean_obj_tag(x_33) == 0)
 {
-uint8_t x_34; 
-x_34 = !lean_is_exclusive(x_33);
-if (x_34 == 0)
+lean_object* x_34; lean_object* x_35; 
+x_34 = lean_ctor_get(x_33, 1);
+lean_inc(x_34);
+lean_dec(x_33);
+lean_inc(x_5);
+x_35 = l_Lean_Meta_mkInjectiveTheorems(x_5, x_15, x_16, x_17, x_18, x_34);
+if (lean_obj_tag(x_35) == 0)
 {
-lean_object* x_35; 
-x_35 = lean_ctor_get(x_33, 0);
+uint8_t x_36; 
+x_36 = !lean_is_exclusive(x_35);
+if (x_36 == 0)
+{
+lean_object* x_37; 
+x_37 = lean_ctor_get(x_35, 0);
+lean_dec(x_37);
+lean_ctor_set(x_35, 0, x_5);
+return x_35;
+}
+else
+{
+lean_object* x_38; lean_object* x_39; 
+x_38 = lean_ctor_get(x_35, 1);
+lean_inc(x_38);
 lean_dec(x_35);
-lean_ctor_set(x_33, 0, x_5);
-return x_33;
-}
-else
-{
-lean_object* x_36; lean_object* x_37; 
-x_36 = lean_ctor_get(x_33, 1);
-lean_inc(x_36);
-lean_dec(x_33);
-x_37 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_37, 0, x_5);
-lean_ctor_set(x_37, 1, x_36);
-return x_37;
+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;
 }
 }
 else
 {
-uint8_t x_38; 
+uint8_t x_40; 
 lean_dec(x_5);
-x_38 = !lean_is_exclusive(x_33);
-if (x_38 == 0)
+x_40 = !lean_is_exclusive(x_35);
+if (x_40 == 0)
 {
-return x_33;
+return x_35;
 }
 else
 {
-lean_object* x_39; lean_object* x_40; lean_object* x_41; 
-x_39 = lean_ctor_get(x_33, 0);
-x_40 = lean_ctor_get(x_33, 1);
-lean_inc(x_40);
-lean_inc(x_39);
-lean_dec(x_33);
-x_41 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_41, 0, x_39);
-lean_ctor_set(x_41, 1, x_40);
-return x_41;
+lean_object* x_41; lean_object* x_42; lean_object* x_43; 
+x_41 = lean_ctor_get(x_35, 0);
+x_42 = lean_ctor_get(x_35, 1);
+lean_inc(x_42);
+lean_inc(x_41);
+lean_dec(x_35);
+x_43 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_43, 0, x_41);
+lean_ctor_set(x_43, 1, x_42);
+return x_43;
 }
 }
 }
 else
 {
-uint8_t x_42; 
+uint8_t x_44; 
 lean_dec(x_18);
 lean_dec(x_17);
 lean_dec(x_16);
 lean_dec(x_15);
-x_42 = !lean_is_exclusive(x_31);
-if (x_42 == 0)
+lean_dec(x_5);
+x_44 = !lean_is_exclusive(x_33);
+if (x_44 == 0)
 {
-lean_object* x_43; 
-x_43 = lean_ctor_get(x_31, 0);
-lean_dec(x_43);
+return x_33;
+}
+else
+{
+lean_object* x_45; lean_object* x_46; lean_object* x_47; 
+x_45 = lean_ctor_get(x_33, 0);
+x_46 = lean_ctor_get(x_33, 1);
+lean_inc(x_46);
+lean_inc(x_45);
+lean_dec(x_33);
+x_47 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_47, 0, x_45);
+lean_ctor_set(x_47, 1, x_46);
+return x_47;
+}
+}
+}
+else
+{
+uint8_t x_48; 
+lean_dec(x_18);
+lean_dec(x_17);
+lean_dec(x_16);
+lean_dec(x_15);
+x_48 = !lean_is_exclusive(x_31);
+if (x_48 == 0)
+{
+lean_object* x_49; 
+x_49 = lean_ctor_get(x_31, 0);
+lean_dec(x_49);
 lean_ctor_set(x_31, 0, x_5);
 return x_31;
 }
 else
 {
-lean_object* x_44; lean_object* x_45; 
-x_44 = lean_ctor_get(x_31, 1);
-lean_inc(x_44);
+lean_object* x_50; lean_object* x_51; 
+x_50 = lean_ctor_get(x_31, 1);
+lean_inc(x_50);
 lean_dec(x_31);
-x_45 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_45, 0, x_5);
-lean_ctor_set(x_45, 1, x_44);
-return x_45;
+x_51 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_51, 0, x_5);
+lean_ctor_set(x_51, 1, x_50);
+return x_51;
 }
 }
 }
 else
 {
-uint8_t x_46; 
+uint8_t x_52; 
 lean_dec(x_18);
 lean_dec(x_17);
 lean_dec(x_16);
 lean_dec(x_15);
 lean_dec(x_5);
-x_46 = !lean_is_exclusive(x_31);
-if (x_46 == 0)
+x_52 = !lean_is_exclusive(x_31);
+if (x_52 == 0)
 {
 return x_31;
 }
 else
 {
-lean_object* x_47; lean_object* x_48; lean_object* x_49; 
-x_47 = lean_ctor_get(x_31, 0);
-x_48 = lean_ctor_get(x_31, 1);
-lean_inc(x_48);
-lean_inc(x_47);
+lean_object* x_53; lean_object* x_54; lean_object* x_55; 
+x_53 = lean_ctor_get(x_31, 0);
+x_54 = lean_ctor_get(x_31, 1);
+lean_inc(x_54);
+lean_inc(x_53);
 lean_dec(x_31);
-x_49 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_49, 0, x_47);
-lean_ctor_set(x_49, 1, x_48);
-return x_49;
+x_55 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_55, 0, x_53);
+lean_ctor_set(x_55, 1, x_54);
+return x_55;
 }
 }
 }
 else
 {
-uint8_t x_50; 
+uint8_t x_56; 
 lean_dec(x_18);
 lean_dec(x_17);
 lean_dec(x_16);
@ -18704,29 +18745,29 @@ lean_dec(x_5);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_50 = !lean_is_exclusive(x_24);
-if (x_50 == 0)
+x_56 = !lean_is_exclusive(x_24);
+if (x_56 == 0)
 {
 return x_24;
 }
 else
 {
-lean_object* x_51; lean_object* x_52; lean_object* x_53; 
-x_51 = lean_ctor_get(x_24, 0);
-x_52 = lean_ctor_get(x_24, 1);
-lean_inc(x_52);
-lean_inc(x_51);
+lean_object* x_57; lean_object* x_58; lean_object* x_59; 
+x_57 = lean_ctor_get(x_24, 0);
+x_58 = lean_ctor_get(x_24, 1);
+lean_inc(x_58);
+lean_inc(x_57);
 lean_dec(x_24);
-x_53 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_53, 0, x_51);
-lean_ctor_set(x_53, 1, x_52);
-return x_53;
+x_59 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_59, 0, x_57);
+lean_ctor_set(x_59, 1, x_58);
+return x_59;
 }
 }
 }
 else
 {
-uint8_t x_54; 
+uint8_t x_60; 
 lean_dec(x_18);
 lean_dec(x_17);
 lean_dec(x_16);
@ -18742,23 +18783,23 @@ lean_dec(x_5);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_54 = !lean_is_exclusive(x_22);
-if (x_54 == 0)
+x_60 = !lean_is_exclusive(x_22);
+if (x_60 == 0)
 {
 return x_22;
 }
 else
 {
-lean_object* x_55; lean_object* x_56; lean_object* x_57; 
-x_55 = lean_ctor_get(x_22, 0);
-x_56 = lean_ctor_get(x_22, 1);
-lean_inc(x_56);
-lean_inc(x_55);
+lean_object* x_61; lean_object* x_62; lean_object* x_63; 
+x_61 = lean_ctor_get(x_22, 0);
+x_62 = lean_ctor_get(x_22, 1);
+lean_inc(x_62);
+lean_inc(x_61);
 lean_dec(x_22);
-x_57 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_57, 0, x_55);
-lean_ctor_set(x_57, 1, x_56);
-return x_57;
+x_63 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_63, 0, x_61);
+lean_ctor_set(x_63, 1, x_62);
+return x_63;
 }
 }
 }
@ -19973,7 +20014,7 @@ lean_dec(x_8);
 return x_15;
 }
 }
-lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_4848_(lean_object* x_1) {
+lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_4860_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
@ -19986,6 +20027,7 @@ lean_object* initialize_Init(lean_object*);
 lean_object* initialize_Lean_Parser_Command(lean_object*);
 lean_object* initialize_Lean_Meta_Closure(lean_object*);
 lean_object* initialize_Lean_Meta_SizeOf(lean_object*);
+lean_object* initialize_Lean_Meta_Injective(lean_object*);
 lean_object* initialize_Lean_Elab_Command(lean_object*);
 lean_object* initialize_Lean_Elab_DeclModifiers(lean_object*);
 lean_object* initialize_Lean_Elab_DeclUtil(lean_object*);
@ -20008,6 +20050,9 @@ lean_dec_ref(res);
 res = initialize_Lean_Meta_SizeOf(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Lean_Meta_Injective(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 res = initialize_Lean_Elab_Command(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
@ -20170,7 +20215,7 @@ l_Lean_Elab_Command_elabStructure___lambda__4___closed__1 = _init_l_Lean_Elab_Co
 lean_mark_persistent(l_Lean_Elab_Command_elabStructure___lambda__4___closed__1);
 l_Lean_Elab_Command_elabStructure___closed__1 = _init_l_Lean_Elab_Command_elabStructure___closed__1();
 lean_mark_persistent(l_Lean_Elab_Command_elabStructure___closed__1);
-res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_4848_(lean_io_mk_world());
+res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_4860_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));
--- a/stage0/stdlib/Lean/Meta/Injective.c
+++ b/stage0/stdlib/Lean/Meta/Injective.c
--- a/stage0/stdlib/Lean/Meta/Tactic/Apply.c
+++ b/stage0/stdlib/Lean/Meta/Tactic/Apply.c
@ -26,8 +26,10 @@ lean_object* l_Lean_Meta_apply_match__1(lean_object*);
 lean_object* l_Lean_Meta_getExpectedNumArgs(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_getExpectedNumArgs_match__1___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_getParamNames___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_applyRefl_match__1(lean_object*);
 lean_object* l___private_Lean_Meta_Tactic_Apply_0__Lean_Meta_throwApplyError___rarg___closed__3;
 lean_object* l___private_Lean_Meta_Tactic_Apply_0__Lean_Meta_throwApplyError(lean_object*);
+lean_object* l_Lean_Meta_saveState___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_apply___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Meta_Tactic_Apply_0__Lean_Meta_dependsOnOthers___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Array_empty___closed__1;
@ -37,8 +39,10 @@ uint8_t lean_name_eq(lean_object*, lean_object*);
 lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
 lean_object* l_ReaderT_bind___at_Lean_Meta_instMonadLCtxMetaM___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_observing_x3f___at_Lean_Meta_splitAnd___spec__1___at_Lean_Meta_splitAnd___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_getExpectedNumArgs_match__1(lean_object*);
 lean_object* l_Lean_Meta_apply___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_applyRefl___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_checkNotAssigned___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_appendTag(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_postprocessAppMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -57,13 +61,17 @@ lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Meta_Tactic_Apply_0__Lea
 lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Meta_Tactic_Apply_0__Lean_Meta_reorderNonDependentFirst___spec__1(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_getMVarType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_FindMVar_main___at___private_Lean_Meta_Tactic_Apply_0__Lean_Meta_dependsOnOthers___spec__1___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_applyRefl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_headBetaMVarType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_getMVarsNoDelayed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallMetaTelescopeReducingAux(lean_object*, uint8_t, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_splitAnd___closed__1;
+extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_23346____closed__4;
 lean_object* lean_nat_sub(lean_object*, lean_object*);
 lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_apply___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_FindMVar_visit(lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_observing_x3f___at_Lean_Meta_splitAnd___spec__1___at_Lean_Meta_splitAnd___spec__2___closed__1;
 lean_object* l_Lean_FindMVar_main___at___private_Lean_Meta_Tactic_Apply_0__Lean_Meta_dependsOnOthers___spec__1___lambda__1___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_apply___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* l_Lean_Meta_apply_match__1___rarg(lean_object*, lean_object*);
@ -75,15 +83,21 @@ lean_object* l___private_Lean_Meta_Tactic_Apply_0__Lean_Meta_throwApplyError___r
 lean_object* l___private_Lean_Meta_Tactic_Apply_0__Lean_Meta_throwApplyError___rarg___closed__2;
 extern lean_object* l_Lean_KernelException_toMessageData___closed__15;
 lean_object* l___private_Lean_Meta_Tactic_Apply_0__Lean_Meta_throwApplyError___rarg___closed__1;
+lean_object* l_Lean_Meta_applyRefl___lambda__2___closed__1;
 lean_object* l_Nat_forM_loop___at_Lean_Meta_synthAppInstances___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Nat_forM_loop___at_Lean_Meta_synthAppInstances___spec__1___closed__2;
+lean_object* l_Lean_Meta_applyRefl___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_BinderInfo_isInstImplicit(uint8_t);
+extern lean_object* l_Lean_Meta_mkEqRefl___closed__1;
+lean_object* l_Lean_Meta_saturate(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_SavedState_restore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_getExpectedNumArgsAux___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 size_t lean_usize_of_nat(lean_object*);
 lean_object* l_Lean_Meta_getExpectedNumArgsAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Nat_forM_loop___at_Lean_Meta_synthAppInstances___spec__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* l_Lean_Meta_apply___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_postprocessAppMVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_Meta_mkEqRefl___closed__2;
 lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_apply___spec__4(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_throwTacticEx___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern uint8_t l_Lean_instInhabitedBinderInfo;
@ -109,7 +123,9 @@ lean_object* l_Lean_Meta_inferType(lean_object*, lean_object*, lean_object*, lea
 lean_object* l_Lean_Meta_isExprDefEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Tactic_apply___closed__1;
 lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_applyRefl___closed__1;
 extern lean_object* l_Array_unzip___rarg___closed__1;
+lean_object* l_Lean_Meta_applyRefl_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Meta_Tactic_Apply_0__Lean_Meta_reorderNonDependentFirst_match__1(lean_object*);
 lean_object* l___private_Lean_Meta_Tactic_Apply_0__Lean_Meta_reorderNonDependentFirst_match__1___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Expr_getAppFn(lean_object*);
@ -118,7 +134,12 @@ lean_object* l___private_Lean_Meta_Tactic_Apply_0__Lean_Meta_throwApplyError___r
 lean_object* l_Nat_forM_loop___at_Lean_Meta_appendParentTag___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_indentExpr(lean_object*);
 lean_object* l_Lean_Meta_setMVarTag(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_mkConst(lean_object*, lean_object*);
+lean_object* l_Lean_Meta_splitAnd(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Nat_forM_loop___at_Lean_Meta_appendParentTag___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_observing_x3f___at_Lean_Meta_splitAnd___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_applyRefl___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_mkFreshLevelMVar___boxed(lean_object*);
 lean_object* l_Lean_Meta_appendParentTag(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 lean_object* l_List_forM___at_Lean_Meta_apply___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -3037,6 +3058,355 @@ lean_dec(x_4);
 return x_10;
 }
 }
+lean_object* l_Lean_observing_x3f___at_Lean_Meta_splitAnd___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) {
+_start:
+{
+lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; 
+x_7 = l_Lean_Meta_saveState___rarg(x_3, x_4, x_5, x_6);
+x_8 = lean_ctor_get(x_7, 0);
+lean_inc(x_8);
+x_9 = lean_ctor_get(x_7, 1);
+lean_inc(x_9);
+lean_dec(x_7);
+lean_inc(x_5);
+lean_inc(x_4);
+lean_inc(x_3);
+lean_inc(x_2);
+x_10 = lean_apply_5(x_1, x_2, x_3, x_4, x_5, x_9);
+if (lean_obj_tag(x_10) == 0)
+{
+uint8_t x_11; 
+lean_dec(x_8);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+x_11 = !lean_is_exclusive(x_10);
+if (x_11 == 0)
+{
+lean_object* x_12; lean_object* x_13; 
+x_12 = lean_ctor_get(x_10, 0);
+x_13 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_13, 0, x_12);
+lean_ctor_set(x_10, 0, x_13);
+return x_10;
+}
+else
+{
+lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; 
+x_14 = lean_ctor_get(x_10, 0);
+x_15 = lean_ctor_get(x_10, 1);
+lean_inc(x_15);
+lean_inc(x_14);
+lean_dec(x_10);
+x_16 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_16, 0, x_14);
+x_17 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_17, 0, x_16);
+lean_ctor_set(x_17, 1, x_15);
+return x_17;
+}
+}
+else
+{
+lean_object* x_18; lean_object* x_19; uint8_t x_20; 
+x_18 = lean_ctor_get(x_10, 1);
+lean_inc(x_18);
+lean_dec(x_10);
+x_19 = l_Lean_Meta_SavedState_restore(x_8, x_2, x_3, x_4, x_5, x_18);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_8);
+x_20 = !lean_is_exclusive(x_19);
+if (x_20 == 0)
+{
+lean_object* x_21; lean_object* x_22; 
+x_21 = lean_ctor_get(x_19, 0);
+lean_dec(x_21);
+x_22 = lean_box(0);
+lean_ctor_set(x_19, 0, x_22);
+return x_19;
+}
+else
+{
+lean_object* x_23; lean_object* x_24; lean_object* x_25; 
+x_23 = lean_ctor_get(x_19, 1);
+lean_inc(x_23);
+lean_dec(x_19);
+x_24 = lean_box(0);
+x_25 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_25, 0, x_24);
+lean_ctor_set(x_25, 1, x_23);
+return x_25;
+}
+}
+}
+}
+static lean_object* _init_l_Lean_observing_x3f___at_Lean_Meta_splitAnd___spec__1___at_Lean_Meta_splitAnd___spec__2___closed__1() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_23346____closed__4;
+x_3 = l_Lean_mkConst(x_2, x_1);
+return x_3;
+}
+}
+lean_object* l_Lean_observing_x3f___at_Lean_Meta_splitAnd___spec__1___at_Lean_Meta_splitAnd___spec__2(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; lean_object* x_10; lean_object* x_11; 
+x_7 = l_Lean_Meta_saveState___rarg(x_3, x_4, x_5, x_6);
+x_8 = lean_ctor_get(x_7, 0);
+lean_inc(x_8);
+x_9 = lean_ctor_get(x_7, 1);
+lean_inc(x_9);
+lean_dec(x_7);
+x_10 = l_Lean_observing_x3f___at_Lean_Meta_splitAnd___spec__1___at_Lean_Meta_splitAnd___spec__2___closed__1;
+lean_inc(x_5);
+lean_inc(x_4);
+lean_inc(x_3);
+lean_inc(x_2);
+x_11 = l_Lean_Meta_apply(x_1, x_10, x_2, x_3, x_4, x_5, x_9);
+if (lean_obj_tag(x_11) == 0)
+{
+uint8_t x_12; 
+lean_dec(x_8);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+x_12 = !lean_is_exclusive(x_11);
+if (x_12 == 0)
+{
+lean_object* x_13; lean_object* x_14; 
+x_13 = lean_ctor_get(x_11, 0);
+x_14 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_14, 0, x_13);
+lean_ctor_set(x_11, 0, x_14);
+return x_11;
+}
+else
+{
+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(1, 1, 0);
+lean_ctor_set(x_17, 0, x_15);
+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_19; lean_object* x_20; uint8_t x_21; 
+x_19 = lean_ctor_get(x_11, 1);
+lean_inc(x_19);
+lean_dec(x_11);
+x_20 = l_Lean_Meta_SavedState_restore(x_8, x_2, x_3, x_4, x_5, x_19);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_8);
+x_21 = !lean_is_exclusive(x_20);
+if (x_21 == 0)
+{
+lean_object* x_22; lean_object* x_23; 
+x_22 = lean_ctor_get(x_20, 0);
+lean_dec(x_22);
+x_23 = lean_box(0);
+lean_ctor_set(x_20, 0, x_23);
+return x_20;
+}
+else
+{
+lean_object* x_24; lean_object* x_25; lean_object* x_26; 
+x_24 = lean_ctor_get(x_20, 1);
+lean_inc(x_24);
+lean_dec(x_20);
+x_25 = lean_box(0);
+x_26 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_26, 0, x_25);
+lean_ctor_set(x_26, 1, x_24);
+return x_26;
+}
+}
+}
+}
+static lean_object* _init_l_Lean_Meta_splitAnd___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_observing_x3f___at_Lean_Meta_splitAnd___spec__1___at_Lean_Meta_splitAnd___spec__2), 6, 0);
+return x_1;
+}
+}
+lean_object* l_Lean_Meta_splitAnd(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; 
+x_7 = l_Lean_Meta_splitAnd___closed__1;
+x_8 = l_Lean_Meta_saturate(x_1, x_7, x_2, x_3, x_4, x_5, x_6);
+return x_8;
+}
+}
+lean_object* l_Lean_Meta_applyRefl_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_4; 
+lean_dec(x_2);
+x_4 = lean_apply_1(x_3, x_1);
+return x_4;
+}
+else
+{
+lean_object* x_5; 
+x_5 = lean_ctor_get(x_1, 0);
+lean_inc(x_5);
+if (lean_obj_tag(x_5) == 0)
+{
+lean_object* x_6; lean_object* x_7; 
+lean_dec(x_3);
+lean_dec(x_1);
+x_6 = lean_box(0);
+x_7 = lean_apply_1(x_2, x_6);
+return x_7;
+}
+else
+{
+lean_object* x_8; 
+lean_dec(x_5);
+lean_dec(x_2);
+x_8 = lean_apply_1(x_3, x_1);
+return x_8;
+}
+}
+}
+}
+lean_object* l_Lean_Meta_applyRefl_match__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_Meta_applyRefl_match__1___rarg), 3, 0);
+return x_2;
+}
+}
+lean_object* l_Lean_Meta_applyRefl___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; lean_object* x_11; lean_object* x_12; 
+x_8 = lean_box(0);
+x_9 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_9, 0, x_2);
+lean_ctor_set(x_9, 1, x_8);
+x_10 = l_Lean_Meta_mkEqRefl___closed__2;
+x_11 = l_Lean_mkConst(x_10, x_9);
+x_12 = l_Lean_Meta_apply(x_1, x_11, x_3, x_4, x_5, x_6, x_7);
+return x_12;
+}
+}
+static lean_object* _init_l_Lean_Meta_applyRefl___lambda__2___closed__1() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Lean_Meta_mkEqRefl___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+lean_object* l_Lean_Meta_applyRefl___lambda__2(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:
+{
+if (lean_obj_tag(x_3) == 0)
+{
+lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+x_9 = l_Lean_Meta_applyRefl___lambda__2___closed__1;
+x_10 = lean_box(0);
+x_11 = l_Lean_Meta_throwTacticEx___rarg(x_9, x_1, x_2, x_10, x_4, x_5, x_6, x_7, x_8);
+return x_11;
+}
+else
+{
+lean_object* x_12; 
+x_12 = lean_ctor_get(x_3, 0);
+if (lean_obj_tag(x_12) == 0)
+{
+lean_object* x_13; lean_object* x_14; 
+lean_dec(x_2);
+lean_dec(x_1);
+x_13 = lean_box(0);
+x_14 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_14, 0, x_13);
+lean_ctor_set(x_14, 1, x_8);
+return x_14;
+}
+else
+{
+lean_object* x_15; lean_object* x_16; lean_object* x_17; 
+x_15 = l_Lean_Meta_applyRefl___lambda__2___closed__1;
+x_16 = lean_box(0);
+x_17 = l_Lean_Meta_throwTacticEx___rarg(x_15, x_1, x_2, x_16, x_4, x_5, x_6, x_7, x_8);
+return x_17;
+}
+}
+}
+}
+static lean_object* _init_l_Lean_Meta_applyRefl___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Lean_Meta_mkFreshLevelMVar___boxed), 1, 0);
+return x_1;
+}
+}
+lean_object* l_Lean_Meta_applyRefl(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; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; 
+lean_inc(x_1);
+x_8 = lean_alloc_closure((void*)(l_Lean_Meta_applyRefl___lambda__1), 7, 1);
+lean_closure_set(x_8, 0, x_1);
+x_9 = l_Lean_Meta_applyRefl___closed__1;
+x_10 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Meta_instMonadLCtxMetaM___spec__2___rarg), 7, 2);
+lean_closure_set(x_10, 0, x_9);
+lean_closure_set(x_10, 1, x_8);
+x_11 = lean_alloc_closure((void*)(l_Lean_observing_x3f___at_Lean_Meta_splitAnd___spec__1), 6, 1);
+lean_closure_set(x_11, 0, x_10);
+lean_inc(x_1);
+x_12 = lean_alloc_closure((void*)(l_Lean_Meta_applyRefl___lambda__2___boxed), 8, 2);
+lean_closure_set(x_12, 0, x_1);
+lean_closure_set(x_12, 1, x_2);
+x_13 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Meta_instMonadLCtxMetaM___spec__2___rarg), 7, 2);
+lean_closure_set(x_13, 0, x_11);
+lean_closure_set(x_13, 1, x_12);
+x_14 = l_Lean_Meta_withMVarContext___at_Lean_Meta_admit___spec__1___rarg(x_1, x_13, x_3, x_4, x_5, x_6, x_7);
+return x_14;
+}
+}
+lean_object* l_Lean_Meta_applyRefl___lambda__2___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:
+{
+lean_object* x_9; 
+x_9 = l_Lean_Meta_applyRefl___lambda__2(x_1, x_2, x_3, 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);
+lean_dec(x_3);
+return x_9;
+}
+}
 lean_object* initialize_Init(lean_object*);
 lean_object* initialize_Lean_Util_FindMVar(lean_object*);
 lean_object* initialize_Lean_Meta_ExprDefEq(lean_object*);
@ -3084,6 +3454,14 @@ l___private_Lean_Meta_Tactic_Apply_0__Lean_Meta_reorderNonDependentFirst___close
 lean_mark_persistent(l___private_Lean_Meta_Tactic_Apply_0__Lean_Meta_reorderNonDependentFirst___closed__1);
 l___private_Lean_Meta_Tactic_Apply_0__Lean_Meta_reorderNonDependentFirst___closed__2 = _init_l___private_Lean_Meta_Tactic_Apply_0__Lean_Meta_reorderNonDependentFirst___closed__2();
 lean_mark_persistent(l___private_Lean_Meta_Tactic_Apply_0__Lean_Meta_reorderNonDependentFirst___closed__2);
+l_Lean_observing_x3f___at_Lean_Meta_splitAnd___spec__1___at_Lean_Meta_splitAnd___spec__2___closed__1 = _init_l_Lean_observing_x3f___at_Lean_Meta_splitAnd___spec__1___at_Lean_Meta_splitAnd___spec__2___closed__1();
+lean_mark_persistent(l_Lean_observing_x3f___at_Lean_Meta_splitAnd___spec__1___at_Lean_Meta_splitAnd___spec__2___closed__1);
+l_Lean_Meta_splitAnd___closed__1 = _init_l_Lean_Meta_splitAnd___closed__1();
+lean_mark_persistent(l_Lean_Meta_splitAnd___closed__1);
+l_Lean_Meta_applyRefl___lambda__2___closed__1 = _init_l_Lean_Meta_applyRefl___lambda__2___closed__1();
+lean_mark_persistent(l_Lean_Meta_applyRefl___lambda__2___closed__1);
+l_Lean_Meta_applyRefl___closed__1 = _init_l_Lean_Meta_applyRefl___closed__1();
+lean_mark_persistent(l_Lean_Meta_applyRefl___closed__1);
 return lean_io_result_mk_ok(lean_box(0));
 }
 #ifdef __cplusplus
--- a/stage0/stdlib/Lean/Meta/Tactic/Cases.c
+++ b/stage0/stdlib/Lean/Meta/Tactic/Cases.c
--- a/stage0/stdlib/Lean/Meta/Tactic/Util.c
+++ b/stage0/stdlib/Lean/Meta/Tactic/Util.c
--- a/stage0/stdlib/Lean/Parser/Command.c
+++ b/stage0/stdlib/Lean/Parser/Command.c
@ -310,6 +310,7 @@ lean_object* l_Lean_Parser_Command_mutual___closed__8;
 lean_object* l_Lean_Parser_Tactic_set__option_formatter___closed__5;
 lean_object* l_Lean_Parser_Command_visibility_formatter___closed__2;
 lean_object* l_Lean_Parser_Tactic_open_parenthesizer___closed__5;
+extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__2;
 lean_object* l_Lean_Parser_Command_partial___elambda__1___closed__7;
 lean_object* l_Lean_Parser_Command_namespace___elambda__1___closed__11;
 lean_object* l_Lean_Parser_Command_export___closed__8;
@ -451,6 +452,7 @@ lean_object* l_Lean_Parser_Command_theorem___elambda__1___closed__9;
 lean_object* l_Lean_Parser_Command_abbrev;
 lean_object* l_Lean_Parser_Command_mutual_parenthesizer___closed__11;
 lean_object* l_Lean_Parser_Command_variable_parenthesizer___closed__3;
+extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__1;
 lean_object* l_Lean_Parser_Command_structExplicitBinder___elambda__1___closed__14;
 lean_object* l_Lean_Parser_tokenWithAntiquotFn(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_structExplicitBinder_formatter___closed__9;
@ -1025,7 +1027,6 @@ lean_object* l_Lean_Parser_Command_structure_parenthesizer___closed__9;
 lean_object* l_Lean_Parser_Command_protected_formatter___closed__2;
 lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__10;
 lean_object* l_Lean_Parser_Command_initialize_formatter___closed__1;
-extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__1;
 lean_object* l_Lean_Parser_Command_inferMod___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Command_declaration_parenthesizer___closed__19;
 lean_object* l___regBuiltin_Lean_Parser_Command_in_parenthesizer___closed__1;
@ -1523,7 +1524,6 @@ lean_object* l_Lean_Parser_Command_instance___elambda__1___closed__8;
 lean_object* l_Lean_Parser_Command_declModifiers___closed__3;
 lean_object* l___regBuiltin_Lean_Parser_Command_printAxioms_parenthesizer(lean_object*);
 lean_object* l_Lean_Parser_Command_end___closed__7;
-extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__2;
 lean_object* l_Lean_Parser_Command_end_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_exit___closed__7;
 extern lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__5;
@ -43961,7 +43961,7 @@ static lean_object* _init_l_Lean_Parser_Command_builtin__initialize___elambda__1
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__2;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__2;
 x_2 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_2, 0, x_1);
 return x_2;
@ -43971,7 +43971,7 @@ static lean_object* _init_l_Lean_Parser_Command_builtin__initialize___elambda__1
 _start:
 {
 lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__1;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__1;
 x_2 = l_Lean_Parser_Command_builtin__initialize___elambda__1___closed__1;
 x_3 = 1;
 x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
@ -44031,7 +44031,7 @@ static lean_object* _init_l_Lean_Parser_Command_builtin__initialize___elambda__1
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__2;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__2;
 x_2 = l_Lean_Parser_Command_builtin__initialize___elambda__1___closed__7;
 x_3 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn), 4, 2);
 lean_closure_set(x_3, 0, x_1);
@ -44167,7 +44167,7 @@ if (x_22 == 0)
 {
 lean_object* x_23; lean_object* x_24; lean_object* x_25; uint8_t x_26; 
 lean_dec(x_4);
-x_23 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__2;
+x_23 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__2;
 x_24 = l_Lean_Parser_ParserState_mkNode(x_20, x_23, x_14);
 x_25 = lean_ctor_get(x_24, 4);
 lean_inc(x_25);
@ -44198,7 +44198,7 @@ lean_dec(x_29);
 if (x_30 == 0)
 {
 lean_object* x_31; lean_object* x_32; lean_object* x_33; uint8_t x_34; 
-x_31 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__2;
+x_31 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__2;
 x_32 = l_Lean_Parser_ParserState_mkNode(x_28, x_31, x_14);
 x_33 = lean_ctor_get(x_32, 4);
 lean_inc(x_33);
@ -44225,7 +44225,7 @@ x_37 = l_Lean_Parser_Term_doSeqIndent___closed__5;
 x_38 = 1;
 lean_inc(x_1);
 x_39 = l_Lean_Parser_orelseFnCore(x_36, x_37, x_38, x_1, x_28);
-x_40 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__2;
+x_40 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__2;
 x_41 = l_Lean_Parser_ParserState_mkNode(x_39, x_40, x_14);
 x_42 = lean_ctor_get(x_41, 4);
 lean_inc(x_42);
@ -44282,7 +44282,7 @@ static lean_object* _init_l_Lean_Parser_Command_builtin__initialize___closed__3(
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__2;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__2;
 x_2 = l_Lean_Parser_Command_builtin__initialize___closed__2;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
@ -44353,7 +44353,7 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_4146____closed__4;
-x_3 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__2;
+x_3 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__2;
 x_4 = 1;
 x_5 = l_Lean_Parser_Command_builtin__initialize;
 x_6 = lean_unsigned_to_nat(1000u);
@ -44365,7 +44365,7 @@ static lean_object* _init_l_Lean_Parser_Command_builtin__initialize_formatter___
 _start:
 {
 lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__1;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__1;
 x_2 = l_Lean_Parser_Command_builtin__initialize___elambda__1___closed__1;
 x_3 = 1;
 x_4 = lean_box(x_3);
@ -44402,7 +44402,7 @@ static lean_object* _init_l_Lean_Parser_Command_builtin__initialize_formatter___
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__2;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__2;
 x_2 = lean_unsigned_to_nat(1024u);
 x_3 = l_Lean_Parser_Command_builtin__initialize_formatter___closed__3;
 x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
@ -44435,7 +44435,7 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_2 = l_Lean_PrettyPrinter_formatterAttribute;
-x_3 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__2;
+x_3 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__2;
 x_4 = l___regBuiltin_Lean_Parser_Command_builtin__initialize_formatter___closed__1;
 x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
@ -44445,7 +44445,7 @@ static lean_object* _init_l_Lean_Parser_Command_builtin__initialize_parenthesize
 _start:
 {
 lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__1;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__1;
 x_2 = l_Lean_Parser_Command_builtin__initialize___elambda__1___closed__1;
 x_3 = 1;
 x_4 = lean_box(x_3);
@ -44482,7 +44482,7 @@ static lean_object* _init_l_Lean_Parser_Command_builtin__initialize_parenthesize
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__2;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__2;
 x_2 = lean_unsigned_to_nat(1024u);
 x_3 = l_Lean_Parser_Command_builtin__initialize_parenthesizer___closed__3;
 x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
@ -44515,7 +44515,7 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_2 = l_Lean_PrettyPrinter_parenthesizerAttribute;
-x_3 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__2;
+x_3 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__2;
 x_4 = l___regBuiltin_Lean_Parser_Command_builtin__initialize_parenthesizer___closed__1;
 x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
--- a/stage0/stdlib/Lean/Parser/Do.c
+++ b/stage0/stdlib/Lean/Parser/Do.c
@ -213,6 +213,7 @@ lean_object* l_Lean_Parser_Term_doAssert;
 lean_object* l_Lean_Parser_Term_notFollowedByRedefinedTermToken___elambda__1___closed__34;
 lean_object* l_Lean_Parser_Term_doIf_parenthesizer___closed__17;
 lean_object* l___regBuiltinParser_Lean_Parser_Term_doTry(lean_object*);
+extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__11;
 lean_object* l_Lean_Parser_Term_doTry___elambda__1___closed__17;
 lean_object* l_Lean_Parser_Term_doDbgTrace___closed__4;
 extern lean_object* l_Lean_Parser_minPrec;
@ -397,7 +398,6 @@ lean_object* l_Lean_Parser_Term_doIfLetBind___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Term_doCatchMatch___closed__3;
 lean_object* l_Lean_Parser_Term_doIfCond___closed__3;
 lean_object* l_Lean_Parser_Term_doAssert___closed__1;
-extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__11;
 lean_object* l_Lean_Parser_unicodeSymbol_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_doMatch_formatter___closed__2;
 lean_object* l_Lean_Parser_Term_liftMethod___elambda__1___closed__5;
@ -495,6 +495,7 @@ lean_object* l_Lean_Parser_Term_doCatch___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Term_doUnless___elambda__1___closed__7;
 lean_object* l_Lean_Parser_optional_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_doTry___elambda__1___closed__3;
+extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__12;
 lean_object* l_Lean_Parser_Term_doIfLetBind___elambda__1___closed__8;
 lean_object* l_Lean_Parser_Term_doIf___elambda__1___closed__37;
 lean_object* l_Lean_Parser_Term_doTry_formatter___closed__11;
@ -653,7 +654,6 @@ lean_object* l_Lean_Parser_Term_doDbgTrace_parenthesizer___closed__2;
 lean_object* l_Lean_Parser_Term_doUnless_parenthesizer___closed__7;
 lean_object* l_Lean_Parser_Term_doContinue___closed__3;
 lean_object* l___regBuiltin_Lean_Parser_Term_doHave_parenthesizer___closed__1;
-extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__12;
 lean_object* l_Lean_Parser_Term_doElem_quot_parenthesizer___closed__3;
 extern lean_object* l_Lean_Parser_Term_optType;
 lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Do___hyg_4_(lean_object*);
@ -713,7 +713,6 @@ lean_object* l_Lean_Parser_Term_doIf_formatter___closed__9;
 lean_object* l_Lean_Parser_Term_doHave_formatter___closed__2;
 lean_object* l_Lean_Parser_Term_doBreak_formatter___closed__3;
 lean_object* l_Lean_Parser_Term_doSeqIndent_formatter___closed__1;
-extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__8;
 lean_object* l_Lean_Parser_Term_notFollowedByRedefinedTermToken___elambda__1___closed__51;
 lean_object* l_Lean_Parser_Term_doLetArrow_parenthesizer___closed__2;
 lean_object* l_Lean_Parser_Term_doLet___elambda__1___closed__10;
@ -1094,6 +1093,7 @@ lean_object* l_Lean_Parser_Term_doLet___closed__5;
 lean_object* l_Lean_Parser_Term_doIf_parenthesizer___closed__1;
 lean_object* l_Lean_Parser_Term_liftMethod___elambda__1___closed__9;
 lean_object* l_Lean_Parser_Term_doBreak___closed__4;
+extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__10;
 lean_object* l_Lean_Parser_Term_termUnless___closed__2;
 extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_23499____closed__1;
 lean_object* l_Lean_Parser_Term_doDbgTrace___closed__7;
@ -1143,7 +1143,6 @@ lean_object* l_Lean_Parser_Term_doFinally___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Term_doContinue___elambda__1___closed__10;
 extern lean_object* l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_3030____closed__11;
 lean_object* l_Lean_Parser_Term_doFor_parenthesizer___closed__2;
-extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__9;
 lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Do___hyg_4____closed__2;
 lean_object* l_Lean_Parser_Term_doTry___closed__7;
 lean_object* l_Lean_Parser_Term_liftMethod___elambda__1___closed__8;
@ -1229,7 +1228,6 @@ lean_object* l_Lean_Parser_Term_leftArrow;
 lean_object* l_Lean_Parser_Term_doTry_parenthesizer___closed__8;
 lean_object* l_Lean_Parser_Term_doAssert___closed__5;
 extern lean_object* l_Lean_Parser_Term_have___elambda__1___closed__3;
-extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13;
 lean_object* l_Lean_Parser_Term_doReassignArrow___closed__1;
 lean_object* l___regBuiltin_Lean_Parser_Term_doReassign_parenthesizer(lean_object*);
 uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_671____at_Lean_Parser_ParserState_hasError___spec__1(lean_object*, lean_object*);
@ -1456,7 +1454,6 @@ lean_object* l_Lean_Parser_Term_doUnless___elambda__1___closed__10;
 lean_object* l_Lean_Parser_Term_notFollowedByRedefinedTermToken___elambda__1___closed__35;
 lean_object* l_Lean_Parser_Term_doBreak_formatter___closed__1;
 lean_object* l_Lean_Parser_Term_doIf_parenthesizer___closed__11;
-extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__10;
 lean_object* l_Lean_Parser_Term_doLet___closed__8;
 lean_object* l_Lean_Parser_Term_doSeqBracketed___elambda__1___closed__5;
 extern lean_object* l_Lean_Parser_Term_letPatDecl_formatter___closed__2;
@ -1608,6 +1605,7 @@ lean_object* l_Lean_Parser_Term_doLet___elambda__1___closed__2;
 extern lean_object* l_Lean_Parser_Term_type___elambda__1___closed__6;
 lean_object* l_Lean_Parser_mkAntiquot(lean_object*, lean_object*, uint8_t);
 lean_object* l_Lean_Parser_Term_doNested___closed__3;
+extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13;
 lean_object* l_Lean_Parser_Term_doUnless___elambda__1___closed__21;
 lean_object* l___regBuiltin_Lean_Parser_Term_doExpr_parenthesizer___closed__1;
 lean_object* l_Lean_Parser_Term_doForDecl_parenthesizer___closed__3;
@ -1718,6 +1716,7 @@ lean_object* l_Lean_Parser_Term_doLetArrow_formatter___closed__1;
 lean_object* l_Lean_Parser_Term_doContinue___elambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Term_termTry_formatter___closed__2;
 lean_object* l_Lean_Parser_Term_doIdDecl___elambda__1___closed__11;
+extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__8;
 lean_object* l_Lean_Parser_Term_doIf___elambda__1___closed__23;
 lean_object* l_Lean_Parser_Term_doIf_parenthesizer___closed__6;
 lean_object* l_Lean_Parser_Term_matchAlts_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1910,6 +1909,7 @@ lean_object* l_Lean_Parser_Term_doIf_formatter___closed__5;
 lean_object* l_Lean_Parser_Term_doIf___elambda__1___closed__34;
 lean_object* l_Lean_Parser_Term_doCatch___closed__11;
 lean_object* l_Lean_Parser_Term_liftMethod_formatter___closed__1;
+extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__9;
 lean_object* l_Lean_Parser_Term_doIf___elambda__1___closed__41;
 lean_object* l_Lean_Parser_Term_initFn____x40_Lean_Parser_Do___hyg_193____closed__11;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -2664,7 +2664,7 @@ static lean_object* _init_l_Lean_Parser_Term_doSeqItem___elambda__1___closed__1(
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__11;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__11;
 x_2 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_2, 0, x_1);
 return x_2;
@ -2674,7 +2674,7 @@ static lean_object* _init_l_Lean_Parser_Term_doSeqItem___elambda__1___closed__2(
 _start:
 {
 lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__10;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__10;
 x_2 = l_Lean_Parser_Term_doSeqItem___elambda__1___closed__1;
 x_3 = 1;
 x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
@ -2782,7 +2782,7 @@ static lean_object* _init_l_Lean_Parser_Term_doSeqItem___elambda__1___closed__12
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__11;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__11;
 x_2 = l_Lean_Parser_Term_doSeqItem___elambda__1___closed__11;
 x_3 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn), 4, 2);
 lean_closure_set(x_3, 0, x_1);
@ -2863,7 +2863,7 @@ if (x_19 == 0)
 {
 lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23; 
 lean_dec(x_4);
-x_20 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__11;
+x_20 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__11;
 x_21 = l_Lean_Parser_ParserState_mkNode(x_17, x_20, x_14);
 x_22 = lean_ctor_get(x_21, 4);
 lean_inc(x_22);
@ -2887,7 +2887,7 @@ else
 lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; uint8_t x_29; 
 lean_inc(x_1);
 x_25 = lean_apply_2(x_4, x_1, x_17);
-x_26 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__11;
+x_26 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__11;
 x_27 = l_Lean_Parser_ParserState_mkNode(x_25, x_26, x_14);
 x_28 = lean_ctor_get(x_27, 4);
 lean_inc(x_28);
@ -2957,7 +2957,7 @@ static lean_object* _init_l_Lean_Parser_Term_doSeqItem___closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__11;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__11;
 x_2 = l_Lean_Parser_Term_doSeqItem___closed__3;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
@ -3027,7 +3027,7 @@ static lean_object* _init_l_Lean_Parser_Term_doSeqIndent___elambda__1___closed__
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__9;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__9;
 x_2 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_2, 0, x_1);
 return x_2;
@ -3037,7 +3037,7 @@ static lean_object* _init_l_Lean_Parser_Term_doSeqIndent___elambda__1___closed__
 _start:
 {
 lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__8;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__8;
 x_2 = l_Lean_Parser_Term_doSeqIndent___elambda__1___closed__1;
 x_3 = 1;
 x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
@ -3103,7 +3103,7 @@ static lean_object* _init_l_Lean_Parser_Term_doSeqIndent___elambda__1___closed__
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__9;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__9;
 x_2 = l_Lean_Parser_Term_doSeqIndent___elambda__1___closed__7;
 x_3 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn), 4, 2);
 lean_closure_set(x_3, 0, x_1);
@ -3206,7 +3206,7 @@ lean_ctor_set(x_26, 5, x_25);
 lean_ctor_set(x_26, 6, x_21);
 lean_ctor_set_uint8(x_26, sizeof(void*)*7, x_20);
 x_27 = lean_apply_2(x_15, x_26, x_7);
-x_28 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__9;
+x_28 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__9;
 x_29 = l_Lean_Parser_ParserState_mkNode(x_27, x_28, x_12);
 x_30 = lean_ctor_get(x_29, 4);
 lean_inc(x_30);
@ -3256,7 +3256,7 @@ lean_ctor_set(x_40, 5, x_39);
 lean_ctor_set(x_40, 6, x_21);
 lean_ctor_set_uint8(x_40, sizeof(void*)*7, x_20);
 x_41 = lean_apply_2(x_15, x_40, x_7);
-x_42 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__9;
+x_42 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__9;
 x_43 = l_Lean_Parser_ParserState_mkNode(x_41, x_42, x_12);
 x_44 = lean_ctor_get(x_43, 4);
 lean_inc(x_44);
@ -3331,7 +3331,7 @@ lean_ctor_set(x_59, 5, x_58);
 lean_ctor_set(x_59, 6, x_21);
 lean_ctor_set_uint8(x_59, sizeof(void*)*7, x_20);
 x_60 = lean_apply_2(x_15, x_59, x_7);
-x_61 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__9;
+x_61 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__9;
 x_62 = l_Lean_Parser_ParserState_mkNode(x_60, x_61, x_12);
 x_63 = lean_ctor_get(x_62, 4);
 lean_inc(x_63);
@ -3369,7 +3369,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
 x_1 = l_Lean_Parser_Term_doSeqIndent___elambda__1___closed__6;
 x_2 = lean_ctor_get(x_1, 0);
 lean_inc(x_2);
-x_3 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__9;
+x_3 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__9;
 x_4 = l_Lean_Parser_nodeInfo(x_3, x_2);
 return x_4;
 }
@ -4356,7 +4356,7 @@ static lean_object* _init_l_Lean_Parser_Term_doSeqItem_formatter___closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__10;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__10;
 x_2 = l_Lean_Parser_Term_doSeqItem___elambda__1___closed__1;
 x_3 = 1;
 x_4 = lean_box(x_3);
@ -4423,7 +4423,7 @@ static lean_object* _init_l_Lean_Parser_Term_doSeqItem_formatter___closed__7() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__11;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__11;
 x_2 = lean_unsigned_to_nat(1024u);
 x_3 = l_Lean_Parser_Term_doSeqItem_formatter___closed__6;
 x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
@ -4538,7 +4538,7 @@ static lean_object* _init_l_Lean_Parser_Term_doSeqIndent_formatter___closed__1()
 _start:
 {
 lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__8;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__8;
 x_2 = l_Lean_Parser_Term_doSeqIndent___elambda__1___closed__1;
 x_3 = 1;
 x_4 = lean_box(x_3);
@ -4563,7 +4563,7 @@ static lean_object* _init_l_Lean_Parser_Term_doSeqIndent_formatter___closed__3()
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__9;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__9;
 x_2 = lean_unsigned_to_nat(1024u);
 x_3 = l_Lean_Parser_Term_doSeqIndent_formatter___closed__2;
 x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
@ -4622,7 +4622,7 @@ static lean_object* _init_l_Lean_Parser_Term_doSeqItem_parenthesizer___closed__1
 _start:
 {
 lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__10;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__10;
 x_2 = l_Lean_Parser_Term_doSeqItem___elambda__1___closed__1;
 x_3 = 1;
 x_4 = lean_box(x_3);
@ -4691,7 +4691,7 @@ static lean_object* _init_l_Lean_Parser_Term_doSeqItem_parenthesizer___closed__7
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__11;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__11;
 x_2 = lean_unsigned_to_nat(1024u);
 x_3 = l_Lean_Parser_Term_doSeqItem_parenthesizer___closed__6;
 x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
@ -4806,7 +4806,7 @@ static lean_object* _init_l_Lean_Parser_Term_doSeqIndent_parenthesizer___closed_
 _start:
 {
 lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__8;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__8;
 x_2 = l_Lean_Parser_Term_doSeqIndent___elambda__1___closed__1;
 x_3 = 1;
 x_4 = lean_box(x_3);
@ -4831,7 +4831,7 @@ static lean_object* _init_l_Lean_Parser_Term_doSeqIndent_parenthesizer___closed_
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__9;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__9;
 x_2 = lean_unsigned_to_nat(1024u);
 x_3 = l_Lean_Parser_Term_doSeqIndent_parenthesizer___closed__2;
 x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
@ -26041,7 +26041,7 @@ static lean_object* _init_l_Lean_Parser_Term_doExpr___elambda__1___closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13;
 x_2 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_2, 0, x_1);
 return x_2;
@ -26051,7 +26051,7 @@ static lean_object* _init_l_Lean_Parser_Term_doExpr___elambda__1___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__12;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__12;
 x_2 = l_Lean_Parser_Term_doExpr___elambda__1___closed__1;
 x_3 = 1;
 x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
@ -26188,7 +26188,7 @@ static lean_object* _init_l_Lean_Parser_Term_doExpr___elambda__1___closed__15()
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13;
 x_2 = l_Lean_Parser_Term_doExpr___elambda__1___closed__14;
 x_3 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn), 4, 2);
 lean_closure_set(x_3, 0, x_1);
@ -26262,7 +26262,7 @@ lean_dec(x_14);
 if (x_15 == 0)
 {
 lean_object* x_16; lean_object* x_17; lean_object* x_18; uint8_t x_19; 
-x_16 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13;
+x_16 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13;
 x_17 = l_Lean_Parser_ParserState_mkNode(x_13, x_16, x_12);
 x_18 = lean_ctor_get(x_17, 4);
 lean_inc(x_18);
@ -26295,7 +26295,7 @@ lean_dec(x_24);
 if (x_25 == 0)
 {
 lean_object* x_26; lean_object* x_27; lean_object* x_28; uint8_t x_29; 
-x_26 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13;
+x_26 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13;
 x_27 = l_Lean_Parser_ParserState_mkNode(x_23, x_26, x_12);
 x_28 = lean_ctor_get(x_27, 4);
 lean_inc(x_28);
@ -26321,7 +26321,7 @@ x_31 = l_Lean_Parser_Term_doExpr___elambda__1___closed__10;
 x_32 = l_Lean_Parser_Term_doExpr___elambda__1___closed__11;
 lean_inc(x_1);
 x_33 = l_Lean_Parser_notFollowedByFn(x_31, x_32, x_1, x_23);
-x_34 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13;
+x_34 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13;
 x_35 = l_Lean_Parser_ParserState_mkNode(x_33, x_34, x_12);
 x_36 = lean_ctor_get(x_35, 4);
 lean_inc(x_36);
@ -26381,7 +26381,7 @@ static lean_object* _init_l_Lean_Parser_Term_doExpr___closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13;
 x_2 = l_Lean_Parser_Term_doExpr___closed__2;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
@ -26452,7 +26452,7 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Do___hyg_4____closed__4;
-x_3 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13;
+x_3 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13;
 x_4 = 1;
 x_5 = l_Lean_Parser_Term_doExpr;
 x_6 = lean_unsigned_to_nat(1000u);
@ -26464,7 +26464,7 @@ static lean_object* _init_l_Lean_Parser_Term_doExpr_formatter___closed__1() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__12;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__12;
 x_2 = l_Lean_Parser_Term_doExpr___elambda__1___closed__1;
 x_3 = 1;
 x_4 = lean_box(x_3);
@ -26557,7 +26557,7 @@ static lean_object* _init_l_Lean_Parser_Term_doExpr_formatter___closed__9() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13;
 x_2 = lean_unsigned_to_nat(1024u);
 x_3 = l_Lean_Parser_Term_doExpr_formatter___closed__8;
 x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
@ -26590,7 +26590,7 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_2 = l_Lean_PrettyPrinter_formatterAttribute;
-x_3 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13;
+x_3 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13;
 x_4 = l___regBuiltin_Lean_Parser_Term_doExpr_formatter___closed__1;
 x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
@ -26600,7 +26600,7 @@ static lean_object* _init_l_Lean_Parser_Term_doExpr_parenthesizer___closed__1()
 _start:
 {
 lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__12;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__12;
 x_2 = l_Lean_Parser_Term_doExpr___elambda__1___closed__1;
 x_3 = 1;
 x_4 = lean_box(x_3);
@ -26693,7 +26693,7 @@ static lean_object* _init_l_Lean_Parser_Term_doExpr_parenthesizer___closed__9()
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13;
+x_1 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13;
 x_2 = lean_unsigned_to_nat(1024u);
 x_3 = l_Lean_Parser_Term_doExpr_parenthesizer___closed__8;
 x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
@ -26726,7 +26726,7 @@ _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_2 = l_Lean_PrettyPrinter_parenthesizerAttribute;
-x_3 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13;
+x_3 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13;
 x_4 = l___regBuiltin_Lean_Parser_Term_doExpr_parenthesizer___closed__1;
 x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
 return x_5;
--- a/stage0/stdlib/Lean/Parser/Extra.c
+++ b/stage0/stdlib/Lean/Parser/Extra.c
@ -82,6 +82,7 @@ lean_object* l_Lean_Parser_group_formatter(lean_object*, lean_object*, lean_obje
 extern lean_object* l_Lean_identKind___closed__2;
 lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_634____closed__5;
 lean_object* l_Lean_PrettyPrinter_Formatter_manyNoAntiquot_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__11;
 lean_object* l_Lean_Parser_nameLit_formatter___closed__3;
 lean_object* l_Lean_Parser_termRegister__parser__alias_________closed__8;
 extern lean_object* l_term___u2218_____closed__6;
@ -127,7 +128,6 @@ lean_object* l_Lean_Parser_mkAntiquot_formatter___closed__9;
 lean_object* l_Lean_Parser_strLit_formatter___closed__2;
 lean_object* l_Lean_Parser_termRegister__parser__alias_________closed__2;
 lean_object* l_Lean_Parser_charLit___elambda__1___closed__1;
-extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__11;
 lean_object* l_Lean_Parser_unicodeSymbol_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_numLit___closed__3;
 lean_object* l_Lean_Parser_mkAntiquot_formatter___closed__1;
@ -355,7 +355,6 @@ lean_object* l_Lean_ppHardSpace_formatter___boxed(lean_object*, lean_object*, le
 lean_object* l_Lean_Parser_many1_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_nameLit___elambda__1___closed__1;
 extern lean_object* l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_3030____closed__11;
-extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__9;
 lean_object* l_Lean_Parser_notSymbol(lean_object*);
 lean_object* l_Lean_Parser_sepByElemParser_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_nullKind___closed__2;
@ -382,7 +381,6 @@ lean_object* l_Lean_Parser_myMacro____x40_Lean_Parser_Extra___hyg_276_(lean_obje
 lean_object* l_Lean_Parser_numLit;
 lean_object* l_Lean_Parser_many___closed__4;
 lean_object* l_Lean_Parser_charLit_formatter___closed__1;
-extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13;
 uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_671____at_Lean_Parser_ParserState_hasError___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_634____closed__39;
 lean_object* l_Lean_Parser_numLit___elambda__1(lean_object*, lean_object*);
@ -490,6 +488,7 @@ extern lean_object* l_rawNatLit___closed__6;
 lean_object* l_Lean_Parser_withAntiquotSpliceAndSuffix_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_myMacro____x40_Init_Notation___hyg_2278____closed__4;
 lean_object* l_Lean_Parser_mkAntiquot(lean_object*, lean_object*, uint8_t);
+extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_withPosition_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_myMacro____x40_Lean_Parser_Extra___hyg_276____closed__4;
 lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_634____closed__8;
@ -571,6 +570,7 @@ lean_object* l_Lean_ppDedent_formatter(lean_object*, lean_object*, lean_object*,
 extern lean_object* l_Lean_nameLitKind___closed__1;
 lean_object* l_Lean_Parser_manyIndent_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_myMacro____x40_Lean_Parser_Extra___hyg_276____closed__13;
+extern lean_object* l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__9;
 lean_object* l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_938_(lean_object*);
 lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_1075_(lean_object*);
@ -4202,14 +4202,14 @@ x_33 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_33, 0, x_32);
 lean_ctor_set(x_33, 1, x_31);
 x_34 = lean_array_push(x_19, x_33);
-x_35 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13;
+x_35 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13;
 x_36 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_36, 0, x_35);
 lean_ctor_set(x_36, 1, x_34);
 x_37 = lean_array_push(x_19, x_36);
 x_38 = l_myMacro____x40_Init_Notation___hyg_1481____closed__8;
 x_39 = lean_array_push(x_37, x_38);
-x_40 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__11;
+x_40 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__11;
 x_41 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_41, 0, x_40);
 lean_ctor_set(x_41, 1, x_39);
@ -4287,7 +4287,7 @@ x_82 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_82, 0, x_29);
 lean_ctor_set(x_82, 1, x_81);
 x_83 = lean_array_push(x_19, x_82);
-x_84 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__9;
+x_84 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__9;
 x_85 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_85, 0, x_84);
 lean_ctor_set(x_85, 1, x_83);
@ -4346,14 +4346,14 @@ x_109 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_109, 0, x_108);
 lean_ctor_set(x_109, 1, x_107);
 x_110 = lean_array_push(x_95, x_109);
-x_111 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__13;
+x_111 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__13;
 x_112 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_112, 0, x_111);
 lean_ctor_set(x_112, 1, x_110);
 x_113 = lean_array_push(x_95, x_112);
 x_114 = l_myMacro____x40_Init_Notation___hyg_1481____closed__8;
 x_115 = lean_array_push(x_113, x_114);
-x_116 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__11;
+x_116 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__11;
 x_117 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_117, 0, x_116);
 lean_ctor_set(x_117, 1, x_115);
@ -4431,7 +4431,7 @@ x_158 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_158, 0, x_105);
 lean_ctor_set(x_158, 1, x_157);
 x_159 = lean_array_push(x_95, x_158);
-x_160 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_894____closed__9;
+x_160 = l_Lean_Option_myMacro____x40_Lean_Data_Options___hyg_932____closed__9;
 x_161 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_161, 0, x_160);
 lean_ctor_set(x_161, 1, x_159);
--- a/stage0/stdlib/Lean/PrettyPrinter/Delaborator/Basic.c
+++ b/stage0/stdlib/Lean/PrettyPrinter/Delaborator/Basic.c
--- a/stage0/stdlib/Lean/PrettyPrinter/Delaborator/Builtins.c
+++ b/stage0/stdlib/Lean/PrettyPrinter/Delaborator/Builtins.c
--- a/stage0/stdlib/Lean/Server/FileWorker.c
+++ b/stage0/stdlib/Lean/Server/FileWorker.c
--- a/stage0/stdlib/Lean/Server/Utils.c
+++ b/stage0/stdlib/Lean/Server/Utils.c
--- a/stage0/stdlib/Lean/Server/Watchdog.c
+++ b/stage0/stdlib/Lean/Server/Watchdog.c
@ -27,6 +27,7 @@ lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handle
 lean_object* lean_get_stdin(lean_object*);
 lean_object* l_Std_RBNode_insert___at_Lean_Server_Watchdog_updateFileWorkers___spec__1(lean_object*, lean_object*, lean_object*);
 lean_object* lean_mk_empty_array_with_capacity(lean_object*);
+lean_object* l_Lean_Server_Watchdog_startFileWorker___closed__8;
 lean_object* lean_io_mono_ms_now(lean_object*);
 lean_object* l___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_fromJsonDidOpenTextDocumentParams____x40_Lean_Data_Lsp_TextSync___hyg_92_(lean_object*);
 lean_object* l_Lean_Server_Watchdog_handleDidOpen(lean_object*, lean_object*, lean_object*);
@ -62,6 +63,7 @@ extern lean_object* l_Lean_JsonRpc_instToJsonMessage___closed__6;
 uint8_t l_Lean_Syntax_structEq(lean_object*, lean_object*);
 lean_object* l___private_Lean_Server_Watchdog_0__Lean_Server_Watchdog_forwardMessages_loop(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Server_Watchdog_handleEdits___closed__3;
+extern lean_object* l_Lean_Lsp_instInhabitedRange___closed__1;
 extern lean_object* l_Array_empty___closed__1;
 extern lean_object* l_Lean_JsonRpc_instToJsonErrorCode___closed__16;
 lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handleRequest___spec__6___boxed(lean_object*, lean_object*, lean_object*);
@ -102,6 +104,7 @@ lean_object* l_Std_RBNode_forIn_visit___at_Lean_Server_Watchdog_mainLoop___spec_
 lean_object* l_IO_FS_Stream_readNotificationAs___at_Lean_Server_Watchdog_initAndRunWatchdogAux___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Server_Watchdog_initAndRunWatchdogAux(lean_object*, lean_object*);
 lean_object* l_IO_sleep(uint32_t, lean_object*);
+extern lean_object* l_Lean_Lsp_instFromJsonDiagnosticSeverity___closed__2;
 lean_object* l_Lean_Server_Watchdog_handleNotification___closed__2;
 lean_object* l_IO_throwServerError___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Server_Watchdog_mkLeanServerCapabilities___closed__8;
@ -271,6 +274,7 @@ lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handle
 lean_object* l_Lean_Server_Watchdog_handleEdits___closed__2;
 lean_object* l___private_Lean_Server_Watchdog_0__Lean_Server_Watchdog_forwardMessages_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Server_Watchdog_tryWriteMessage(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*);
+lean_object* l_Lean_Server_publishDiagnostics(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonInitializeParams___spec__5(lean_object*, lean_object*);
 lean_object* l_IO_FS_Stream_writeLspNotification___at_Lean_Server_Watchdog_startFileWorker___spec__5(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_handleEdits___spec__1(lean_object*);
@ -331,6 +335,7 @@ extern lean_object* l_Lean_JsonRpc_instToJsonErrorCode___closed__20;
 lean_object* l_Lean_Server_Watchdog_handleRequest(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_forIn_visit___at_Lean_Server_Watchdog_shutdown___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Server_Watchdog_handleRequest_match__2___rarg___closed__5;
+lean_object* l_Lean_Server_Watchdog_startFileWorker___closed__7;
 lean_object* l_Lean_Server_Watchdog_FileWorker_readMessage_match__2(lean_object*);
 lean_object* l_Lean_Server_Watchdog_runClientTask___lambda__2(lean_object*);
 lean_object* l_Std_RBNode_find___at_Lean_Server_Watchdog_findFileWorker___spec__1(lean_object*, lean_object*);
@ -425,6 +430,7 @@ lean_object* l_Lean_Server_Watchdog_handleNotification_match__1___rarg(lean_obje
 lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonInitializeParams___spec__3(lean_object*, lean_object*);
 lean_object* l_Lean_Server_Watchdog_findFileWorker(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handleNotification___spec__1(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Server_Watchdog_startFileWorker___closed__6;
 lean_object* l_Lean_Server_Watchdog_handleRequest_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_RBNode_ins___at_Lean_Server_Watchdog_handleRequest___spec__4(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Server_Watchdog_initAndRunWatchdog___lambda__2___closed__1;
@ -5179,21 +5185,59 @@ static lean_object* _init_l_Lean_Server_Watchdog_startFileWorker___closed__1() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("--worker");
+x_1 = lean_mk_string("starting new server for file...");
 return x_1;
 }
 }
 static lean_object* _init_l_Lean_Server_Watchdog_startFileWorker___closed__2() {
 _start:
 {
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_1 = lean_box(0);
+x_2 = l_Lean_Lsp_instInhabitedRange___closed__1;
+x_3 = l_Lean_Lsp_instFromJsonDiagnosticSeverity___closed__2;
+x_4 = l_Lean_Server_Watchdog_startFileWorker___closed__1;
+x_5 = lean_alloc_ctor(0, 8, 0);
+lean_ctor_set(x_5, 0, x_2);
+lean_ctor_set(x_5, 1, x_2);
+lean_ctor_set(x_5, 2, x_3);
+lean_ctor_set(x_5, 3, x_1);
+lean_ctor_set(x_5, 4, x_1);
+lean_ctor_set(x_5, 5, x_4);
+lean_ctor_set(x_5, 6, x_1);
+lean_ctor_set(x_5, 7, x_1);
+return x_5;
+}
+}
+static lean_object* _init_l_Lean_Server_Watchdog_startFileWorker___closed__3() {
+_start:
+{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_mkOptionalNode___closed__2;
-x_2 = l_Lean_Server_Watchdog_startFileWorker___closed__1;
+x_2 = l_Lean_Server_Watchdog_startFileWorker___closed__2;
 x_3 = lean_array_push(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Server_Watchdog_startFileWorker___closed__3() {
+static lean_object* _init_l_Lean_Server_Watchdog_startFileWorker___closed__4() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("--worker");
+return x_1;
+}
+}
+static lean_object* _init_l_Lean_Server_Watchdog_startFileWorker___closed__5() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_mkOptionalNode___closed__2;
+x_2 = l_Lean_Server_Watchdog_startFileWorker___closed__4;
+x_3 = lean_array_push(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l_Lean_Server_Watchdog_startFileWorker___closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
@ -5202,7 +5246,7 @@ x_2 = lean_task_pure(x_1);
 return x_2;
 }
 }
-static lean_object* _init_l_Lean_Server_Watchdog_startFileWorker___closed__4() {
+static lean_object* _init_l_Lean_Server_Watchdog_startFileWorker___closed__7() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
@ -5212,7 +5256,7 @@ lean_ctor_set(x_2, 0, x_1);
 return x_2;
 }
 }
-static lean_object* _init_l_Lean_Server_Watchdog_startFileWorker___closed__5() {
+static lean_object* _init_l_Lean_Server_Watchdog_startFileWorker___closed__8() {
 _start:
 {
 lean_object* x_1; 
@ -5223,187 +5267,169 @@ return x_1;
 lean_object* l_Lean_Server_Watchdog_startFileWorker(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
-lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; 
-x_4 = lean_ctor_get(x_1, 0);
-lean_inc(x_4);
-x_5 = lean_ctor_get(x_1, 1);
+lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
+x_4 = lean_box(0);
+x_5 = lean_ctor_get(x_2, 1);
 lean_inc(x_5);
-x_6 = lean_ctor_get(x_1, 2);
-lean_inc(x_6);
-x_7 = lean_ctor_get(x_6, 0);
-lean_inc(x_7);
-lean_dec(x_6);
-lean_inc(x_7);
-x_8 = l___private_Lean_Server_Watchdog_0__Lean_Server_Watchdog_parseHeaderAst(x_7, x_3);
-if (lean_obj_tag(x_8) == 0)
+x_6 = l_Lean_Server_Watchdog_startFileWorker___closed__3;
+lean_inc(x_1);
+x_7 = l_Lean_Server_publishDiagnostics(x_1, x_6, x_5, x_3);
+if (lean_obj_tag(x_7) == 0)
 {
-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; lean_object* x_22; 
-x_9 = lean_ctor_get(x_8, 0);
+lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; 
+x_8 = lean_ctor_get(x_7, 1);
+lean_inc(x_8);
+lean_dec(x_7);
+x_9 = lean_ctor_get(x_1, 0);
 lean_inc(x_9);
-x_10 = lean_ctor_get(x_8, 1);
+x_10 = lean_ctor_get(x_1, 1);
 lean_inc(x_10);
-lean_dec(x_8);
-x_11 = lean_ctor_get(x_2, 7);
+x_11 = lean_ctor_get(x_1, 2);
 lean_inc(x_11);
-x_12 = lean_ctor_get(x_2, 3);
+x_12 = lean_ctor_get(x_11, 0);
 lean_inc(x_12);
-x_13 = l_List_redLength___rarg(x_12);
-x_14 = lean_mk_empty_array_with_capacity(x_13);
-lean_dec(x_13);
-x_15 = l_List_toArrayAux___rarg(x_12, x_14);
-x_16 = l_Lean_Server_Watchdog_startFileWorker___closed__2;
-x_17 = l_Array_append___rarg(x_16, x_15);
-lean_dec(x_15);
-x_18 = lean_box(0);
-x_19 = l_Lean_Server_Watchdog_workerCfg;
-x_20 = l_Array_empty___closed__1;
-x_21 = lean_alloc_ctor(0, 5, 0);
-lean_ctor_set(x_21, 0, x_19);
-lean_ctor_set(x_21, 1, x_11);
-lean_ctor_set(x_21, 2, x_17);
-lean_ctor_set(x_21, 3, x_18);
-lean_ctor_set(x_21, 4, x_20);
-x_22 = lean_io_process_spawn(x_21, x_10);
-if (lean_obj_tag(x_22) == 0)
+lean_dec(x_11);
+lean_inc(x_12);
+x_13 = l___private_Lean_Server_Watchdog_0__Lean_Server_Watchdog_parseHeaderAst(x_12, x_8);
+if (lean_obj_tag(x_13) == 0)
 {
-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; lean_object* x_36; 
-x_23 = lean_ctor_get(x_22, 0);
-lean_inc(x_23);
-x_24 = lean_ctor_get(x_22, 1);
-lean_inc(x_24);
-lean_dec(x_22);
-x_25 = lean_box(0);
-x_26 = l_IO_mkRef___at_Lean_Server_Watchdog_startFileWorker___spec__1(x_25, x_2, x_24);
+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; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; 
+x_14 = lean_ctor_get(x_13, 0);
+lean_inc(x_14);
+x_15 = lean_ctor_get(x_13, 1);
+lean_inc(x_15);
+lean_dec(x_13);
+x_16 = lean_ctor_get(x_2, 7);
+lean_inc(x_16);
+x_17 = lean_ctor_get(x_2, 3);
+lean_inc(x_17);
+x_18 = l_List_redLength___rarg(x_17);
+x_19 = lean_mk_empty_array_with_capacity(x_18);
+lean_dec(x_18);
+x_20 = l_List_toArrayAux___rarg(x_17, x_19);
+x_21 = l_Lean_Server_Watchdog_startFileWorker___closed__5;
+x_22 = l_Array_append___rarg(x_21, x_20);
+lean_dec(x_20);
+x_23 = l_Lean_Server_Watchdog_workerCfg;
+x_24 = l_Array_empty___closed__1;
+x_25 = lean_alloc_ctor(0, 5, 0);
+lean_ctor_set(x_25, 0, x_23);
+lean_ctor_set(x_25, 1, x_16);
+lean_ctor_set(x_25, 2, x_22);
+lean_ctor_set(x_25, 3, x_4);
+lean_ctor_set(x_25, 4, x_24);
+x_26 = lean_io_process_spawn(x_25, x_15);
+if (lean_obj_tag(x_26) == 0)
+{
+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; lean_object* x_40; 
 x_27 = lean_ctor_get(x_26, 0);
 lean_inc(x_27);
 x_28 = lean_ctor_get(x_26, 1);
 lean_inc(x_28);
 lean_dec(x_26);
-x_29 = l_IO_mkRef___at_Lean_Server_Watchdog_startFileWorker___spec__2(x_18, x_2, x_28);
-x_30 = lean_ctor_get(x_29, 0);
-lean_inc(x_30);
-x_31 = lean_ctor_get(x_29, 1);
+x_29 = lean_box(0);
+x_30 = l_IO_mkRef___at_Lean_Server_Watchdog_startFileWorker___spec__1(x_29, x_2, x_28);
+x_31 = lean_ctor_get(x_30, 0);
 lean_inc(x_31);
-lean_dec(x_29);
-x_32 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_32, 0, x_1);
-lean_ctor_set(x_32, 1, x_9);
-x_33 = l_Lean_Server_Watchdog_startFileWorker___closed__3;
-x_34 = lean_box(1);
-lean_inc(x_30);
-lean_inc(x_27);
-lean_inc(x_23);
+x_32 = lean_ctor_get(x_30, 1);
 lean_inc(x_32);
-x_35 = lean_alloc_ctor(0, 6, 0);
-lean_ctor_set(x_35, 0, x_32);
-lean_ctor_set(x_35, 1, x_23);
-lean_ctor_set(x_35, 2, x_33);
-lean_ctor_set(x_35, 3, x_34);
-lean_ctor_set(x_35, 4, x_27);
-lean_ctor_set(x_35, 5, x_30);
-lean_inc(x_2);
-x_36 = l___private_Lean_Server_Watchdog_0__Lean_Server_Watchdog_forwardMessages(x_35, x_2, x_31);
-if (lean_obj_tag(x_36) == 0)
-{
-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; lean_object* x_45; 
-x_37 = lean_ctor_get(x_36, 0);
-lean_inc(x_37);
-x_38 = lean_ctor_get(x_36, 1);
-lean_inc(x_38);
-lean_dec(x_36);
+lean_dec(x_30);
+x_33 = l_IO_mkRef___at_Lean_Server_Watchdog_startFileWorker___spec__2(x_4, x_2, x_32);
+x_34 = lean_ctor_get(x_33, 0);
+lean_inc(x_34);
+x_35 = lean_ctor_get(x_33, 1);
+lean_inc(x_35);
+lean_dec(x_33);
+x_36 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_36, 0, x_1);
+lean_ctor_set(x_36, 1, x_14);
+x_37 = l_Lean_Server_Watchdog_startFileWorker___closed__6;
+x_38 = lean_box(1);
+lean_inc(x_34);
+lean_inc(x_31);
+lean_inc(x_27);
+lean_inc(x_36);
 x_39 = lean_alloc_ctor(0, 6, 0);
-lean_ctor_set(x_39, 0, x_32);
-lean_ctor_set(x_39, 1, x_23);
+lean_ctor_set(x_39, 0, x_36);
+lean_ctor_set(x_39, 1, x_27);
 lean_ctor_set(x_39, 2, x_37);
-lean_ctor_set(x_39, 3, x_34);
-lean_ctor_set(x_39, 4, x_27);
-lean_ctor_set(x_39, 5, x_30);
-lean_inc(x_39);
-x_40 = l_Lean_Server_Watchdog_FileWorker_stdin(x_39);
-x_41 = lean_ctor_get(x_2, 5);
+lean_ctor_set(x_39, 3, x_38);
+lean_ctor_set(x_39, 4, x_31);
+lean_ctor_set(x_39, 5, x_34);
+lean_inc(x_2);
+x_40 = l___private_Lean_Server_Watchdog_0__Lean_Server_Watchdog_forwardMessages(x_39, x_2, x_35);
+if (lean_obj_tag(x_40) == 0)
+{
+lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; 
+x_41 = lean_ctor_get(x_40, 0);
 lean_inc(x_41);
-x_42 = l_Lean_Server_Watchdog_startFileWorker___closed__4;
-x_43 = l_Lean_Parser_Command_initialize___elambda__1___closed__1;
-x_44 = lean_alloc_ctor(0, 3, 0);
-lean_ctor_set(x_44, 0, x_42);
-lean_ctor_set(x_44, 1, x_43);
-lean_ctor_set(x_44, 2, x_41);
-lean_inc(x_40);
-x_45 = l_IO_FS_Stream_writeLspRequest___at_Lean_Server_Watchdog_startFileWorker___spec__3(x_40, x_44, x_38);
-if (lean_obj_tag(x_45) == 0)
-{
-lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; 
-x_46 = lean_ctor_get(x_45, 1);
-lean_inc(x_46);
-lean_dec(x_45);
-x_47 = l_Lean_getBuiltinSearchPath___closed__3;
-x_48 = lean_alloc_ctor(0, 4, 0);
-lean_ctor_set(x_48, 0, x_4);
+x_42 = lean_ctor_get(x_40, 1);
+lean_inc(x_42);
+lean_dec(x_40);
+x_43 = lean_alloc_ctor(0, 6, 0);
+lean_ctor_set(x_43, 0, x_36);
+lean_ctor_set(x_43, 1, x_27);
+lean_ctor_set(x_43, 2, x_41);
+lean_ctor_set(x_43, 3, x_38);
+lean_ctor_set(x_43, 4, x_31);
+lean_ctor_set(x_43, 5, x_34);
+lean_inc(x_43);
+x_44 = l_Lean_Server_Watchdog_FileWorker_stdin(x_43);
+x_45 = lean_ctor_get(x_2, 5);
+lean_inc(x_45);
+x_46 = l_Lean_Server_Watchdog_startFileWorker___closed__7;
+x_47 = l_Lean_Parser_Command_initialize___elambda__1___closed__1;
+x_48 = lean_alloc_ctor(0, 3, 0);
+lean_ctor_set(x_48, 0, x_46);
 lean_ctor_set(x_48, 1, x_47);
-lean_ctor_set(x_48, 2, x_5);
-lean_ctor_set(x_48, 3, x_7);
-x_49 = l_Lean_Server_Watchdog_startFileWorker___closed__5;
-x_50 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_50, 0, x_49);
-lean_ctor_set(x_50, 1, x_48);
-x_51 = l_IO_FS_Stream_writeLspNotification___at_Lean_Server_Watchdog_startFileWorker___spec__5(x_40, x_50, x_46);
-if (lean_obj_tag(x_51) == 0)
+lean_ctor_set(x_48, 2, x_45);
+lean_inc(x_44);
+x_49 = l_IO_FS_Stream_writeLspRequest___at_Lean_Server_Watchdog_startFileWorker___spec__3(x_44, x_48, x_42);
+if (lean_obj_tag(x_49) == 0)
 {
-lean_object* x_52; lean_object* x_53; 
-x_52 = lean_ctor_get(x_51, 1);
-lean_inc(x_52);
-lean_dec(x_51);
-x_53 = l_Lean_Server_Watchdog_updateFileWorkers(x_39, x_2, x_52);
-lean_dec(x_2);
-return x_53;
-}
-else
+lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; 
+x_50 = lean_ctor_get(x_49, 1);
+lean_inc(x_50);
+lean_dec(x_49);
+x_51 = l_Lean_getBuiltinSearchPath___closed__3;
+x_52 = lean_alloc_ctor(0, 4, 0);
+lean_ctor_set(x_52, 0, x_9);
+lean_ctor_set(x_52, 1, x_51);
+lean_ctor_set(x_52, 2, x_10);
+lean_ctor_set(x_52, 3, x_12);
+x_53 = l_Lean_Server_Watchdog_startFileWorker___closed__8;
+x_54 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_54, 0, x_53);
+lean_ctor_set(x_54, 1, x_52);
+x_55 = l_IO_FS_Stream_writeLspNotification___at_Lean_Server_Watchdog_startFileWorker___spec__5(x_44, x_54, x_50);
+if (lean_obj_tag(x_55) == 0)
 {
-uint8_t x_54; 
-lean_dec(x_39);
-lean_dec(x_2);
-x_54 = !lean_is_exclusive(x_51);
-if (x_54 == 0)
-{
-return x_51;
-}
-else
-{
-lean_object* x_55; lean_object* x_56; lean_object* x_57; 
-x_55 = lean_ctor_get(x_51, 0);
-x_56 = lean_ctor_get(x_51, 1);
+lean_object* x_56; lean_object* x_57; 
+x_56 = lean_ctor_get(x_55, 1);
 lean_inc(x_56);
-lean_inc(x_55);
-lean_dec(x_51);
-x_57 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_57, 0, x_55);
-lean_ctor_set(x_57, 1, x_56);
+lean_dec(x_55);
+x_57 = l_Lean_Server_Watchdog_updateFileWorkers(x_43, x_2, x_56);
+lean_dec(x_2);
 return x_57;
 }
-}
-}
 else
 {
 uint8_t x_58; 
-lean_dec(x_40);
-lean_dec(x_39);
-lean_dec(x_7);
-lean_dec(x_5);
-lean_dec(x_4);
+lean_dec(x_43);
 lean_dec(x_2);
-x_58 = !lean_is_exclusive(x_45);
+x_58 = !lean_is_exclusive(x_55);
 if (x_58 == 0)
 {
-return x_45;
+return x_55;
 }
 else
 {
 lean_object* x_59; lean_object* x_60; lean_object* x_61; 
-x_59 = lean_ctor_get(x_45, 0);
-x_60 = lean_ctor_get(x_45, 1);
+x_59 = lean_ctor_get(x_55, 0);
+x_60 = lean_ctor_get(x_55, 1);
 lean_inc(x_60);
 lean_inc(x_59);
-lean_dec(x_45);
+lean_dec(x_55);
 x_61 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_61, 0, x_59);
 lean_ctor_set(x_61, 1, x_60);
@ -5414,27 +5440,25 @@ return x_61;
 else
 {
 uint8_t x_62; 
-lean_dec(x_32);
-lean_dec(x_30);
-lean_dec(x_27);
-lean_dec(x_23);
-lean_dec(x_7);
-lean_dec(x_5);
-lean_dec(x_4);
+lean_dec(x_44);
+lean_dec(x_43);
+lean_dec(x_12);
+lean_dec(x_10);
+lean_dec(x_9);
 lean_dec(x_2);
-x_62 = !lean_is_exclusive(x_36);
+x_62 = !lean_is_exclusive(x_49);
 if (x_62 == 0)
 {
-return x_36;
+return x_49;
 }
 else
 {
 lean_object* x_63; lean_object* x_64; lean_object* x_65; 
-x_63 = lean_ctor_get(x_36, 0);
-x_64 = lean_ctor_get(x_36, 1);
+x_63 = lean_ctor_get(x_49, 0);
+x_64 = lean_ctor_get(x_49, 1);
 lean_inc(x_64);
 lean_inc(x_63);
-lean_dec(x_36);
+lean_dec(x_49);
 x_65 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_65, 0, x_63);
 lean_ctor_set(x_65, 1, x_64);
@ -5445,25 +5469,27 @@ return x_65;
 else
 {
 uint8_t x_66; 
+lean_dec(x_36);
+lean_dec(x_34);
+lean_dec(x_31);
+lean_dec(x_27);
+lean_dec(x_12);
+lean_dec(x_10);
 lean_dec(x_9);
-lean_dec(x_7);
-lean_dec(x_5);
-lean_dec(x_4);
 lean_dec(x_2);
-lean_dec(x_1);
-x_66 = !lean_is_exclusive(x_22);
+x_66 = !lean_is_exclusive(x_40);
 if (x_66 == 0)
 {
-return x_22;
+return x_40;
 }
 else
 {
 lean_object* x_67; lean_object* x_68; lean_object* x_69; 
-x_67 = lean_ctor_get(x_22, 0);
-x_68 = lean_ctor_get(x_22, 1);
+x_67 = lean_ctor_get(x_40, 0);
+x_68 = lean_ctor_get(x_40, 1);
 lean_inc(x_68);
 lean_inc(x_67);
-lean_dec(x_22);
+lean_dec(x_40);
 x_69 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_69, 0, x_67);
 lean_ctor_set(x_69, 1, x_68);
@ -5474,24 +5500,25 @@ return x_69;
 else
 {
 uint8_t x_70; 
-lean_dec(x_7);
-lean_dec(x_5);
-lean_dec(x_4);
+lean_dec(x_14);
+lean_dec(x_12);
+lean_dec(x_10);
+lean_dec(x_9);
 lean_dec(x_2);
 lean_dec(x_1);
-x_70 = !lean_is_exclusive(x_8);
+x_70 = !lean_is_exclusive(x_26);
 if (x_70 == 0)
 {
-return x_8;
+return x_26;
 }
 else
 {
 lean_object* x_71; lean_object* x_72; lean_object* x_73; 
-x_71 = lean_ctor_get(x_8, 0);
-x_72 = lean_ctor_get(x_8, 1);
+x_71 = lean_ctor_get(x_26, 0);
+x_72 = lean_ctor_get(x_26, 1);
 lean_inc(x_72);
 lean_inc(x_71);
-lean_dec(x_8);
+lean_dec(x_26);
 x_73 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_73, 0, x_71);
 lean_ctor_set(x_73, 1, x_72);
@ -5499,6 +5526,59 @@ return x_73;
 }
 }
 }
+else
+{
+uint8_t x_74; 
+lean_dec(x_12);
+lean_dec(x_10);
+lean_dec(x_9);
+lean_dec(x_2);
+lean_dec(x_1);
+x_74 = !lean_is_exclusive(x_13);
+if (x_74 == 0)
+{
+return x_13;
+}
+else
+{
+lean_object* x_75; lean_object* x_76; lean_object* x_77; 
+x_75 = lean_ctor_get(x_13, 0);
+x_76 = lean_ctor_get(x_13, 1);
+lean_inc(x_76);
+lean_inc(x_75);
+lean_dec(x_13);
+x_77 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_77, 0, x_75);
+lean_ctor_set(x_77, 1, x_76);
+return x_77;
+}
+}
+}
+else
+{
+uint8_t x_78; 
+lean_dec(x_2);
+lean_dec(x_1);
+x_78 = !lean_is_exclusive(x_7);
+if (x_78 == 0)
+{
+return x_7;
+}
+else
+{
+lean_object* x_79; lean_object* x_80; lean_object* x_81; 
+x_79 = lean_ctor_get(x_7, 0);
+x_80 = lean_ctor_get(x_7, 1);
+lean_inc(x_80);
+lean_inc(x_79);
+lean_dec(x_7);
+x_81 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_81, 0, x_79);
+lean_ctor_set(x_81, 1, x_80);
+return x_81;
+}
+}
+}
 }
 lean_object* l_IO_mkRef___at_Lean_Server_Watchdog_startFileWorker___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
@ -12573,7 +12653,7 @@ lean_object* l_Lean_Server_Watchdog_handleNotification_match__1___rarg(lean_obje
 _start:
 {
 lean_object* x_6; uint8_t x_7; 
-x_6 = l_Lean_Server_Watchdog_startFileWorker___closed__5;
+x_6 = l_Lean_Server_Watchdog_startFileWorker___closed__8;
 x_7 = lean_string_dec_eq(x_1, x_6);
 if (x_7 == 0)
 {
@ -12749,7 +12829,7 @@ lean_object* l_Lean_Server_Watchdog_handleNotification(lean_object* x_1, lean_ob
 _start:
 {
 lean_object* x_5; uint8_t x_6; 
-x_5 = l_Lean_Server_Watchdog_startFileWorker___closed__5;
+x_5 = l_Lean_Server_Watchdog_startFileWorker___closed__8;
 x_6 = lean_string_dec_eq(x_1, x_5);
 if (x_6 == 0)
 {
@ -19899,6 +19979,12 @@ l_Lean_Server_Watchdog_startFileWorker___closed__4 = _init_l_Lean_Server_Watchdo
 lean_mark_persistent(l_Lean_Server_Watchdog_startFileWorker___closed__4);
 l_Lean_Server_Watchdog_startFileWorker___closed__5 = _init_l_Lean_Server_Watchdog_startFileWorker___closed__5();
 lean_mark_persistent(l_Lean_Server_Watchdog_startFileWorker___closed__5);
+l_Lean_Server_Watchdog_startFileWorker___closed__6 = _init_l_Lean_Server_Watchdog_startFileWorker___closed__6();
+lean_mark_persistent(l_Lean_Server_Watchdog_startFileWorker___closed__6);
+l_Lean_Server_Watchdog_startFileWorker___closed__7 = _init_l_Lean_Server_Watchdog_startFileWorker___closed__7();
+lean_mark_persistent(l_Lean_Server_Watchdog_startFileWorker___closed__7);
+l_Lean_Server_Watchdog_startFileWorker___closed__8 = _init_l_Lean_Server_Watchdog_startFileWorker___closed__8();
+lean_mark_persistent(l_Lean_Server_Watchdog_startFileWorker___closed__8);
 l_Lean_Server_Watchdog_terminateFileWorker___closed__1 = _init_l_Lean_Server_Watchdog_terminateFileWorker___closed__1();
 lean_mark_persistent(l_Lean_Server_Watchdog_terminateFileWorker___closed__1);
 l_Lean_Server_Watchdog_handleEdits___lambda__1___closed__1 = _init_l_Lean_Server_Watchdog_handleEdits___lambda__1___closed__1();