chore: update stage0

stage0/src/Init/Data/List/Control.lean

@@ -108,14 +108,14 @@ def filterMapM {m : Type u → Type v} [Monad m] {α β : Type u} (f : α → m
 filterMapMAux f as.reverse []
 
 @[specialize]
-def foldlM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : (s → α → m s) → s → List α → m s
+def foldlM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : forall (f : s → α → m s) (init : s), List α → m s
 | f, s, [] => pure s
 | f, s, h :: r   => do
   s' ← f s h;
   foldlM f s' r
 
 @[specialize]
-def foldrM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : (α → s → m s) → s → List α → m s
+def foldrM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : forall (f : α → s → m s) (init : s), List α → m s
 | f, s, [] => pure s
 | f, s, h :: r   => do
   s' ← foldrM f s r;

stage0/src/Init/Data/Nat/Basic.lean

@@ -86,15 +86,15 @@ instance : HasMul Nat :=
 | 0,      a => a
 | succ n, a => foldAux n (f (s - (succ n)) a)
 
-@[inline] def fold {α : Type u} (f : Nat → α → α) (n : Nat) (a : α) : α :=
-foldAux f n n a
+@[inline] def fold {α : Type u} (f : Nat → α → α) (n : Nat) (init : α) : α :=
+foldAux f n n init
 
 @[specialize] def foldRevAux {α : Type u} (f : Nat → α → α) : Nat → α → α
 | 0,      a => a
 | succ n, a => foldRevAux n (f n a)
 
-@[inline] def foldRev {α : Type u} (f : Nat → α → α) (n : Nat) (a : α) : α :=
-foldRevAux f n a
+@[inline] def foldRev {α : Type u} (f : Nat → α → α) (n : Nat) (init : α) : α :=
+foldRevAux f n init
 
 @[specialize] def anyAux (f : Nat → Bool) (s : Nat) : Nat → Bool
 | 0      => false

stage0/src/Init/Data/Nat/Control.lean

@@ -29,15 +29,15 @@ forRevMAux f n
 | 0,   a => pure a
 | i+1, a => f (n-i-1) a >>= foldMAux i
 
-@[inline] def foldM {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (a : α) (n : Nat) : m α :=
-foldMAux f n n a
+@[inline] def foldM {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (init : α) (n : Nat) : m α :=
+foldMAux f n n init
 
 @[specialize] def foldRevMAux {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) : Nat → α → m α
 | 0,   a => pure a
 | i+1, a => f i a >>= foldRevMAux i
 
-@[inline] def foldRevM {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (a : α) (n : Nat) : m α :=
-foldRevMAux f n a
+@[inline] def foldRevM {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (init : α) (n : Nat) : m α :=
+foldRevMAux f n init
 
 @[specialize] def allMAux {m} [Monad m] (p : Nat → m Bool) (n : Nat) : Nat → m Bool
 | 0   => pure true

stage0/src/Lean/Elab/Inductive.lean

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -12,32 +13,26 @@ import Lean.Elab.CollectFVars
 import Lean.Elab.DefView
 import Lean.Elab.DeclUtil
 
-namespace Lean
-namespace Elab
-namespace Command
-
+namespace Lean.Elab.Command
 open Meta
 
 def checkValidInductiveModifier (modifiers : Modifiers) : CommandElabM Unit := do
-when modifiers.isNoncomputable $
-  throwError "invalid use of 'noncomputable' in inductive declaration";
-when modifiers.isPartial $
-  throwError "invalid use of 'partial' in inductive declaration";
-unless (modifiers.attrs.size == 0 || (modifiers.attrs.size == 1 && (modifiers.attrs.get! 0).name == `class)) $
-  throwError "invalid use of attributes in inductive declaration";
-pure ()
+if modifiers.isNoncomputable then
+  throwError "invalid use of 'noncomputable' in inductive declaration"
+if modifiers.isPartial then
+  throwError "invalid use of 'partial' in inductive declaration"
+unless modifiers.attrs.size == 0 || (modifiers.attrs.size == 1 && modifiers.attrs[0].name == `class) do
+  throwError "invalid use of attributes in inductive declaration"
 
 def checkValidCtorModifier (modifiers : Modifiers) : CommandElabM Unit := do
-when modifiers.isNoncomputable $
-  throwError "invalid use of 'noncomputable' in constructor declaration";
-when modifiers.isPartial $
-  throwError "invalid use of 'partial' in constructor declaration";
-when modifiers.isUnsafe $
-  throwError "invalid use of 'unsafe' in constructor declaration";
-when (modifiers.attrs.size != 0) $
-  throwError "invalid use of attributes in constructor declaration";
-pure ()
-
+if modifiers.isNoncomputable then
+  throwError "invalid use of 'noncomputable' in constructor declaration"
+if modifiers.isPartial then
+  throwError "invalid use of 'partial' in constructor declaration"
+if modifiers.isUnsafe then
+  throwError "invalid use of 'unsafe' in constructor declaration"
+if modifiers.attrs.size != 0 then
+  throwError "invalid use of attributes in constructor declaration"
 
 structure CtorView :=
 (ref       : Syntax)
@@ -80,37 +75,40 @@ private partial def elabHeaderAux (views : Array InductiveView)
   if h : i < views.size then
     let view := views.get ⟨i, h⟩;
     Term.elabBinders view.binders.getArgs fun params => do
-      lctx ← getLCtx;
-      localInsts ← getLocalInstances;
+      let lctx ← getLCtx
+      let localInsts ← getLocalInstances
       match view.type? with
-      | none         => do
-        u ← mkFreshLevelMVar;
-        let type := mkSort (mkLevelSucc u);
-        elabHeaderAux (i+1) (acc.push { lctx := lctx, localInsts := localInsts, params := params, type := type, view := view })
-      | some typeStx => do
-        type ← Term.elabTerm typeStx none;
-        unlessM (isTypeFormerType type) $
-          throwErrorAt typeStx "invalid inductive type, resultant type is not a sort";
-        elabHeaderAux (i+1) (acc.push { lctx := lctx, localInsts := localInsts, params := params, type := type, view := view })
+      | none         =>
+        let u ← mkFreshLevelMVar
+        let type := mkSort (mkLevelSucc u)
+        elabHeaderAux views (i+1) (acc.push { lctx := lctx, localInsts := localInsts, params := params, type := type, view := view })
+      | some typeStx =>
+        let type ← Term.elabTerm typeStx none
+        unless (← isTypeFormerType type) do
+          throwErrorAt typeStx "invalid inductive type, resultant type is not a sort"
+        elabHeaderAux views (i+1) (acc.push { lctx := lctx, localInsts := localInsts, params := params, type := type, view := view })
   else
     pure acc
 
 private def checkNumParams (rs : Array ElabHeaderResult) : TermElabM Nat := do
-let numParams := (rs.get! 0).params.size;
-rs.forM fun r => unless (r.params.size == numParams) $
-  throwErrorAt r.view.ref "invalid inductive type, number of parameters mismatch in mutually inductive datatypes";
+let numParams := rs[0].params.size
+for r in rs do
+  unless r.params.size == numParams do
+    throwErrorAt r.view.ref "invalid inductive type, number of parameters mismatch in mutually inductive datatypes"
 pure numParams
 
-private def checkUnsafe (rs : Array ElabHeaderResult) : TermElabM Unit :=
-let isUnsafe := (rs.get! 0).view.modifiers.isUnsafe;
-rs.forM fun r => unless (r.view.modifiers.isUnsafe == isUnsafe) $
-  throwErrorAt r.view.ref "invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes"
+private def checkUnsafe (rs : Array ElabHeaderResult) : TermElabM Unit := do
+let isUnsafe := rs[0].view.modifiers.isUnsafe
+for r in rs do
+  unless r.view.modifiers.isUnsafe == isUnsafe do
+    throwErrorAt r.view.ref "invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes"
 
-private def checkLevelNames (views : Array InductiveView) : TermElabM Unit :=
-when (views.size > 1) do
-  let levelNames := (views.get! 0).levelNames;
-  views.forM fun view => unless (view.levelNames == levelNames) $
-    throwErrorAt view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes"
+private def checkLevelNames (views : Array InductiveView) : TermElabM Unit := do
+if views.size > 1 then
+  let levelNames := views[0].levelNames
+  for view in views do
+    unless view.levelNames == levelNames do
+      throwErrorAt view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes"
 
 private def mkTypeFor (r : ElabHeaderResult) : TermElabM Expr := do
 withLCtx r.lctx r.localInsts do
@@ -129,70 +127,66 @@ forallTelescopeReducing firstType fun _ firstTypeResult => isDefEq firstTypeResu
 
 -- Auxiliary function for checking whether the types in mutually inductive declaration are compatible.
 private partial def checkParamsAndResultType (type firstType : Expr) (numParams : Nat) : TermElabM Unit := do
+try
+  forallTelescopeCompatible type firstType numParams fun _ type firstType =>
+  forallTelescopeReducing type fun _ type =>
+  forallTelescopeReducing firstType fun _ firstType => do
+  match type with
+  | Expr.sort _ _        =>
+    unless (← isDefEq firstType type) do
+      throwError! "resulting universe mismatch, given{indentExpr type}\nexpected type{indentExpr firstType}"
+  | _ =>
+    throwError "unexpected inductive resulting type"
 catch
-  (do forallTelescopeCompatible type firstType numParams fun _ type firstType =>
-      forallTelescopeReducing type fun _ type =>
-      forallTelescopeReducing firstType fun _ firstType =>
-      match type with
-      | Expr.sort _ _        =>
-        unlessM (isDefEq firstType type) $
-          throwError ("resulting universe mismatch, given " ++ indentExpr type ++ Format.line ++ "expected type" ++ indentExpr firstType)
-      | _ =>
-        throwError "unexpected inductive resulting type")
-  (fun ex => match ex with
-    | Exception.error ref msg => throw (Exception.error ref ("invalid mutually inductive types, " ++ msg))
-    | _ => throw ex)
+  | Exception.error ref msg => throw (Exception.error ref msg!"invalid mutually inductive types, {msg}")
+  | ex => throw ex
 
 -- Auxiliary function for checking whether the types in mutually inductive declaration are compatible.
 private def checkHeader (r : ElabHeaderResult) (numParams : Nat) (firstType? : Option Expr) : TermElabM Expr := do
-type ← mkTypeFor r;
+let type ← mkTypeFor r
 match firstType? with
 | none           => pure type
-| some firstType => do
-  withRef r.view.ref $ checkParamsAndResultType type firstType numParams;
+| some firstType =>
+  withRef r.view.ref $ checkParamsAndResultType type firstType numParams
   pure firstType
 
 -- Auxiliary function for checking whether the types in mutually inductive declaration are compatible.
 private partial def checkHeaders (rs : Array ElabHeaderResult) (numParams : Nat) : Nat → Option Expr → TermElabM Unit
-| i, firstType? => when (i < rs.size) do
-  type ← checkHeader (rs.get! i) numParams firstType?;
-  checkHeaders (i+1) type
+| i, firstType? => do
+  if i < rs.size then
+    let type ← checkHeader rs[i] numParams firstType?
+    checkHeaders rs numParams (i+1) type
 
 private def elabHeader (views : Array InductiveView) : TermElabM (Array ElabHeaderResult) := do
-rs ← elabHeaderAux views 0 #[];
-when (rs.size > 1) do {
-  checkUnsafe rs;
-  numParams ← checkNumParams rs;
+let rs ← elabHeaderAux views 0 #[]
+if rs.size > 1 then
+  checkUnsafe rs
+  let numParams ← checkNumParams rs
   checkHeaders rs numParams 0 none
-};
 pure rs
 
-private partial def withInductiveLocalDeclsAux {α} (namesAndTypes : Array (Name × Expr)) (params : Array Expr)
-    (x : Array Expr → Array Expr → TermElabM α) : Nat → Array Expr → TermElabM α
-| i, indFVars =>
-  if h : i < namesAndTypes.size then do
-    let (id, type) := namesAndTypes.get ⟨i, h⟩;
-    withLocalDeclD id type fun indFVar => withInductiveLocalDeclsAux (i+1) (indFVars.push indFVar)
-  else
-    x params indFVars
-
 /- Create a local declaration for each inductive type in `rs`, and execute `x params indFVars`, where `params` are the inductive type parameters and
    `indFVars` are the new local declarations.
    We use the the local context/instances and parameters of rs[0].
    Note that this method is executed after we executed `checkHeaders` and established all
    parameters are compatible. -/
-private def withInductiveLocalDecls {α} (rs : Array ElabHeaderResult) (x : Array Expr → Array Expr → TermElabM α) : TermElabM α := do
-namesAndTypes ← rs.mapM fun r => do {
-  type ← mkTypeFor r;
+private partial def withInductiveLocalDecls {α} (rs : Array ElabHeaderResult) (x : Array Expr → Array Expr → TermElabM α) : TermElabM α := do
+let namesAndTypes ← rs.mapM fun r => do
+  let type ← mkTypeFor r
   pure (r.view.shortDeclName, type)
-};
-let r0     := rs.get! 0;
-let params := r0.params;
-withLCtx r0.lctx r0.localInsts $ withRef r0.view.ref $
-  withInductiveLocalDeclsAux namesAndTypes params x 0 #[]
+let r0     := rs[0]
+let params := r0.params
+withLCtx r0.lctx r0.localInsts $ withRef r0.view.ref do
+  let rec loop (i : Nat) (indFVars : Array Expr) := do
+    if h : i < namesAndTypes.size then
+      let (id, type) := namesAndTypes.get ⟨i, h⟩
+      withLocalDeclD id type fun indFVar => loop (i+1) (indFVars.push indFVar)
+    else
+      x params indFVars
+  loop 0 #[]
 
 private def isInductiveFamily (numParams : Nat) (indFVar : Expr) : TermElabM Bool := do
-indFVarType ← inferType indFVar;
+let indFVarType ← inferType indFVar
 forallTelescopeReducing indFVarType fun xs _ =>
   pure $ xs.size > numParams
 
@@ -205,33 +199,30 @@ forallTelescopeReducing indFVarType fun xs _ =>
   - Universe constraints (the kernel checks for it). -/
 private def elabCtors (indFVar : Expr) (params : Array Expr) (r : ElabHeaderResult) : TermElabM (List Constructor) :=
 withRef r.view.ref do
-indFamily ← isInductiveFamily params.size indFVar;
+let indFamily ← isInductiveFamily params.size indFVar
 r.view.ctors.toList.mapM fun ctorView => Term.elabBinders ctorView.binders.getArgs fun ctorParams =>
-  withRef ctorView.ref $ do
-  type ← match ctorView.type? with
-    | none          => do
-      when indFamily $
-        throwError "constructor resulting type must be specified in inductive family declaration";
+  withRef ctorView.ref do
+  let type ← match ctorView.type? with
+    | none          =>
+      if indFamily then
+        throwError "constructor resulting type must be specified in inductive family declaration"
       pure (mkAppN indFVar params)
-    | some ctorType => do {
-      type ← Term.elabTerm ctorType none;
-      resultingType ← getResultingType type;
-      unless (resultingType.getAppFn == indFVar) $
-        throwError ("unexpected constructor resulting type" ++ indentExpr resultingType);
-      unlessM (isType resultingType) $
-        throwError ("unexpected constructor resulting type, type expected" ++ indentExpr resultingType);
-      let args := resultingType.getAppArgs;
-      params.size.forM fun i => do {
-        let param := params.get! i;
-        let arg   := args.get! i;
-        unlessM (isDefEq param arg) $
-          throwError ("inductive datatype parameter mismatch" ++ indentExpr arg ++ Format.line ++ "expected" ++ indentExpr param);
-        pure ()
-      };
+    | some ctorType =>
+      let type ← Term.elabTerm ctorType none
+      let resultingType ← getResultingType type
+      unless resultingType.getAppFn == indFVar do
+        throwError! "unexpected constructor resulting type{indentExpr resultingType}"
+      unless (← isType resultingType) do
+        throwError! "unexpected constructor resulting type, type expected{indentExpr resultingType}"
+      let args := resultingType.getAppArgs
+      for i in [:params.size] do
+        let param := params[i]
+        let arg   := args[i]
+        unless (← isDefEq param arg) do
+          throwError! "inductive datatype parameter mismatch{indentExpr arg}\nexpected{indentExpr param}"
       pure type
-    };
-  type ← mkForallFVars ctorParams type;
-  type ← mkForallFVars params type;
+  let type ← mkForallFVars ctorParams type
+  let type ← mkForallFVars params type
   pure { name := ctorView.declName, type := type }
 
 /- Convert universe metavariables occurring in the `indTypes` into new parameters.
@@ -239,11 +230,10 @@ r.view.ctors.toList.mapM fun ctorView => Term.elabBinders ctorView.binders.getAr
    `inferResultingUniverse`. -/
 private def levelMVarToParamAux (indTypes : List InductiveType) : StateRefT Nat TermElabM (List InductiveType) :=
 indTypes.mapM fun indType => do
-  type  ← Term.levelMVarToParam' indType.type;
-  ctors ← indType.ctors.mapM fun ctor => do {
-    ctorType ← Term.levelMVarToParam' ctor.type;
+  let type  ← Term.levelMVarToParam' indType.type
+  let ctors ← indType.ctors.mapM fun ctor => do
+    let ctorType ← Term.levelMVarToParam' ctor.type
     pure { ctor with type := ctorType }
-  };
   pure { indType with ctors := ctors, type := type }
 
 private def levelMVarToParam (indTypes : List InductiveType) : TermElabM (List InductiveType) :=
@@ -252,7 +242,7 @@ private def levelMVarToParam (indTypes : List InductiveType) : TermElabM (List I
 private def getResultingUniverse : List InductiveType → TermElabM Level
 | []           => throwError "unexpected empty inductive declaration"
 | indType :: _ => do
-  r ← getResultingType indType.type;
+  let r ← getResultingType indType.type
   match r with
   | Expr.sort u _ => pure u
   | _             => throwError "unexpected inductive type resulting type"
@@ -264,15 +254,14 @@ def tmpIndParam := mkLevelParam `_tmp_ind_univ_param
   Return false if `u` does not contain universe metavariables.
   Throw exception otherwise. -/
 def shouldInferResultUniverse (u : Level) : TermElabM Bool := do
-u ← instantiateLevelMVars u;
+let u ← instantiateLevelMVars u
 if u.hasMVar then
   match u.getLevelOffset with
   | Level.mvar mvarId _ => do
-    Term.assignLevelMVar mvarId tmpIndParam;
+    Term.assignLevelMVar mvarId tmpIndParam
     pure true
   | _ =>
-    throwError $
-      "cannot infer resulting universe level of inductive datatype, given level contains metavariables " ++ mkSort u ++ ", provide universe explicitly"
+    throwError! "cannot infer resulting universe level of inductive datatype, given level contains metavariables {mkSort u}, provide universe explicitly"
 else
   pure false
 
@@ -296,17 +285,17 @@ def accLevelAtCtor : Level → Level → Nat → Array Level → Except String (
 /- Auxiliary function for `updateResultingUniverse` -/
 private partial def collectUniversesFromCtorTypeAux (r : Level) (rOffset : Nat) : Nat → Expr → Array Level → TermElabM (Array Level)
 | 0,   Expr.forallE n d b c, us => do
-  u ← getLevel d;
-  u ← instantiateLevelMVars u;
+  let u ← getLevel d
+  let u ← instantiateLevelMVars u
   match accLevelAtCtor u r rOffset us with
   | Except.error msg => throwError msg
   | Except.ok us     => withLocalDecl n c.binderInfo d $ fun x =>
-    let e := b.instantiate1 x;
-    collectUniversesFromCtorTypeAux 0 e us
+    let e := b.instantiate1 x
+    collectUniversesFromCtorTypeAux r rOffset 0 e us
 | i+1, Expr.forallE n d b c, us => do
-  withLocalDecl n c.binderInfo d $ fun x =>
-    let e := b.instantiate1 x;
-    collectUniversesFromCtorTypeAux i e us
+  withLocalDecl n c.binderInfo d fun x =>
+    let e := b.instantiate1 x
+    collectUniversesFromCtorTypeAux r rOffset i e us
 | _, _, us => pure us
 
 /- Auxiliary function for `updateResultingUniverse` -/
@@ -316,178 +305,161 @@ collectUniversesFromCtorTypeAux r rOffset numParams ctorType us
 
 /- Auxiliary function for `updateResultingUniverse` -/
 private partial def collectUniverses (r : Level) (rOffset : Nat) (numParams : Nat) (indTypes : List InductiveType) : TermElabM (Array Level) :=
-indTypes.foldlM
-  (fun us indType => indType.ctors.foldlM
-    (fun us ctor => collectUniversesFromCtorType r rOffset ctor.type numParams us)
-    us)
-  #[]
+indTypes.foldlM (init := #[]) fun us indType =>
+  indType.ctors.foldlM (init := us) fun us ctor =>
+    collectUniversesFromCtorType r rOffset ctor.type numParams us
 
 private def updateResultingUniverse (numParams : Nat) (indTypes : List InductiveType) : TermElabM (List InductiveType) := do
-r ← getResultingUniverse indTypes;
-let rOffset : Nat   := r.getOffset;
-let r       : Level := r.getLevelOffset;
-unless (r.isParam) $
-  throwError "failed to compute resulting universe level of inductive datatype, provide universe explicitly";
-us ← collectUniverses r rOffset numParams indTypes;
-let rNew := Level.mkNaryMax us.toList;
-let updateLevel (e : Expr) : Expr := e.replaceLevel fun u => if u == tmpIndParam then some rNew else none;
-pure $ indTypes.map fun indType =>
+let r ← getResultingUniverse indTypes
+let rOffset : Nat   := r.getOffset
+let r       : Level := r.getLevelOffset
+unless r.isParam do
+  throwError "failed to compute resulting universe level of inductive datatype, provide universe explicitly"
+let us ← collectUniverses r rOffset numParams indTypes
+let rNew := Level.mkNaryMax us.toList
+let updateLevel (e : Expr) : Expr := e.replaceLevel fun u => if u == tmpIndParam then some rNew else none
+return indTypes.map fun indType =>
   let type := updateLevel indType.type;
   let ctors := indType.ctors.map fun ctor => { ctor with type := updateLevel ctor.type };
   { indType with type := type, ctors := ctors }
 
 private def traceIndTypes (indTypes : List InductiveType) : TermElabM Unit :=
 indTypes.forM fun indType =>
-  indType.ctors.forM fun ctor => IO.println ("  >> " ++ toString ctor.name ++ " : " ++ toString ctor.type)
+  indType.ctors.forM fun ctor => IO.println s!"  >> {ctor.name} : {ctor.type}"
 
 private def collectUsed (indTypes : List InductiveType) : StateRefT CollectFVars.State TermElabM Unit := do
 indTypes.forM fun indType => do
-    Term.collectUsedFVars indType.type;
-    indType.ctors.forM fun ctor => Term.collectUsedFVars ctor.type
+  Term.collectUsedFVars indType.type
+  indType.ctors.forM fun ctor =>
+    Term.collectUsedFVars ctor.type
 
 private def removeUnused (vars : Array Expr) (indTypes : List InductiveType) : TermElabM (LocalContext × LocalInstances × Array Expr) := do
-(_, used) ← (collectUsed indTypes).run {};
+let (_, used) ← (collectUsed indTypes).run {}
 Term.removeUnused vars used
 
 private def withUsed {α} (vars : Array Expr) (indTypes : List InductiveType) (k : Array Expr → TermElabM α) : TermElabM α := do
-(lctx, localInsts, vars) ← removeUnused vars indTypes;
+let (lctx, localInsts, vars) ← removeUnused vars indTypes
 withLCtx lctx localInsts $ k vars
 
 private def updateParams (vars : Array Expr) (indTypes : List InductiveType) : TermElabM (List InductiveType) :=
 indTypes.mapM fun indType => do
-  type ← mkForallFVars vars indType.type;
-  ctors ← indType.ctors.mapM fun ctor => do {
-    ctorType ← mkForallFVars vars ctor.type;
+  let type ← mkForallFVars vars indType.type
+  let ctors ← indType.ctors.mapM fun ctor => do
+    let ctorType ← mkForallFVars vars ctor.type
     pure { ctor with type := ctorType }
-  };
   pure { indType with type := type, ctors := ctors }
 
 private def collectLevelParamsInInductive (indTypes : List InductiveType) : Array Name :=
-let usedParams := indTypes.foldl
-  (fun (usedParams : CollectLevelParams.State) indType =>
-    let usedParams := collectLevelParams usedParams indType.type;
-    indType.ctors.foldl
-      (fun (usedParams : CollectLevelParams.State) ctor => collectLevelParams usedParams ctor.type)
-      usedParams)
-  {};
+let usedParams := indTypes.foldl (init := {}) fun (usedParams : CollectLevelParams.State) indType =>
+  let usedParams := collectLevelParams usedParams indType.type;
+  indType.ctors.foldl (init := usedParams) fun (usedParams : CollectLevelParams.State) ctor =>
+    collectLevelParams usedParams ctor.type
 usedParams.params
 
 private def mkIndFVar2Const (views : Array InductiveView) (indFVars : Array Expr) (levelNames : List Name) : ExprMap Expr :=
 let levelParams := levelNames.map mkLevelParam;
-views.size.fold
-  (fun i (m : ExprMap Expr) =>
-    let view    := views.get! i;
-    let indFVar := indFVars.get! i;
-    m.insert indFVar (mkConst view.declName levelParams))
-  {}
+views.size.fold (init := {}) fun i (m : ExprMap Expr) =>
+  let view    := views[i]
+  let indFVar := indFVars[i]
+  m.insert indFVar (mkConst view.declName levelParams)
 
 /- Remark: `numVars <= numParams`. `numVars` is the number of context `variables` used in the inductive declaration,
    and `numParams` is `numVars` + number of explicit parameters provided in the declaration. -/
 private def replaceIndFVarsWithConsts (views : Array InductiveView) (indFVars : Array Expr) (levelNames : List Name)
     (numVars : Nat) (numParams : Nat) (indTypes : List InductiveType) : TermElabM (List InductiveType) :=
-let indFVar2Const := mkIndFVar2Const views indFVars levelNames;
+let indFVar2Const := mkIndFVar2Const views indFVars levelNames
 indTypes.mapM fun indType => do
-  ctors ← indType.ctors.mapM fun ctor => do {
-     type ← forallBoundedTelescope ctor.type numParams fun params type => do {
+  let ctors ← indType.ctors.mapM fun ctor => do
+    let type ← forallBoundedTelescope ctor.type numParams fun params type => do
       let type := type.replace fun e =>
         if !e.isFVar then
           none
         else match indFVar2Const.find? e with
           | none   => none
-          | some c => mkAppN c (params.extract 0 numVars);
+          | some c => mkAppN c (params.extract 0 numVars)
       mkForallFVars params type
-    };
     pure { ctor with type := type }
-  };
   pure { indType with ctors := ctors }
 
 abbrev Ctor2InferMod := Std.HashMap Name Bool
 
 private def mkCtor2InferMod (views : Array InductiveView) : Ctor2InferMod :=
-views.foldl
-  (fun (m : Ctor2InferMod) view => view.ctors.foldl
-    (fun (m : Ctor2InferMod) ctorView => m.insert ctorView.declName ctorView.inferMod)
-    m)
-  {}
+views.foldl (init := {}) fun m view =>
+  view.ctors.foldl (init := m) fun m ctorView =>
+    m.insert ctorView.declName ctorView.inferMod
 
 private def applyInferMod (views : Array InductiveView) (numParams : Nat) (indTypes : List InductiveType) : List InductiveType :=
-let ctor2InferMod := mkCtor2InferMod views;
+let ctor2InferMod := mkCtor2InferMod views
 indTypes.map fun indType =>
   let ctors := indType.ctors.map fun ctor =>
-    let inferMod := ctor2InferMod.find! ctor.name; -- true if `{}` was used
-    let ctorType := ctor.type.inferImplicit numParams !inferMod;
-    { ctor with type := ctorType };
+    let inferMod := ctor2InferMod.find! ctor.name -- true if `{}` was used
+    let ctorType := ctor.type.inferImplicit numParams !inferMod
+    { ctor with type := ctorType }
   { indType with ctors := ctors }
 
 private def mkAuxConstructions (views : Array InductiveView) : TermElabM Unit := do
-env ← getEnv;
-let hasEq   := env.contains `Eq;
-let hasHEq  := env.contains `HEq;
-let hasUnit := env.contains `PUnit;
-let hasProd := env.contains `Prod;
-views.forM fun view => do {
+let env ← getEnv
+let hasEq   := env.contains `Eq
+let hasHEq  := env.contains `HEq
+let hasUnit := env.contains `PUnit
+let hasProd := env.contains `Prod
+for view in views do
+  let n := view.declName
+  modifyEnv fun env => mkRecOn env n
+  if hasUnit then modifyEnv fun env => mkCasesOn env n
+  if hasUnit && hasEq && hasHEq then modifyEnv fun env => mkNoConfusion env n
+  if hasUnit && hasProd then modifyEnv fun env => mkBelow env n
+  if hasUnit && hasProd then modifyEnv fun env => mkIBelow env n
+for view in views do
   let n := view.declName;
-  modifyEnv fun env => mkRecOn env n;
-  when hasUnit $ modifyEnv fun env => mkCasesOn env n;
-  when (hasUnit && hasEq && hasHEq) $ modifyEnv fun env => mkNoConfusion env n;
-  when (hasUnit && hasProd) $ modifyEnv fun env => mkBelow env n;
-  when (hasUnit && hasProd) $ modifyEnv fun env => mkIBelow env n;
-  pure ()
-};
-views.forM fun view => do {
-  let n := view.declName;
-  when (hasUnit && hasProd) $ modifyEnv fun env => mkBRecOn env n;
-  when (hasUnit && hasProd) $ modifyEnv fun env => mkBInductionOn env n;
-  pure ()
-}
+  if hasUnit && hasProd then modifyEnv fun env => mkBRecOn env n
+  if hasUnit && hasProd then modifyEnv fun env => mkBInductionOn env n
 
 private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) : TermElabM Unit := do
-let view0             := views.get! 0;
-scopeLevelNames ← Term.getLevelNames;
-checkLevelNames views;
-let allUserLevelNames := view0.levelNames;
-let isUnsafe          := view0.modifiers.isUnsafe;
+let view0 := views[0]
+let scopeLevelNames ← Term.getLevelNames
+checkLevelNames views
+let allUserLevelNames := view0.levelNames
+let isUnsafe          := view0.modifiers.isUnsafe
 withRef view0.ref $ Term.withLevelNames allUserLevelNames do
-  rs ← elabHeader views;
+  let rs ← elabHeader views
   withInductiveLocalDecls rs fun params indFVars => do
-    let numExplicitParams := params.size;
-    indTypes ← views.size.foldM
-      (fun i (indTypes : List InductiveType) => do
-        let indFVar := indFVars.get! i;
-        let r       := rs.get! i;
-        type  ← mkForallFVars params r.type;
-        ctors ← elabCtors indFVar params r;
-        let indType := { name := r.view.declName, type := type, ctors := ctors : InductiveType };
-        pure (indType :: indTypes))
-      [];
-    let indTypes := indTypes.reverse;
-    Term.synthesizeSyntheticMVarsNoPostponing;
-    u ← getResultingUniverse indTypes;
-    inferLevel ← shouldInferResultUniverse u;
-    withUsed vars indTypes $ fun vars => do
-      let numVars   := vars.size;
-      let numParams := numVars + numExplicitParams;
-      indTypes ← updateParams vars indTypes;
-      indTypes ← levelMVarToParam indTypes;
-      indTypes ← if inferLevel then updateResultingUniverse numParams indTypes else pure indTypes;
-      let usedLevelNames := collectLevelParamsInInductive indTypes;
+    let numExplicitParams := params.size
+    let indTypes ← views.size.foldM (init := []) fun i (indTypes : List InductiveType) => do
+      let indFVar := indFVars[i]
+      let r       := rs[i]
+      let type  ← mkForallFVars params r.type
+      let ctors ← elabCtors indFVar params r
+      let indType := { name := r.view.declName, type := type, ctors := ctors : InductiveType }
+      pure (indType :: indTypes)
+    let indTypes := indTypes.reverse
+    Term.synthesizeSyntheticMVarsNoPostponing
+    let u ← getResultingUniverse indTypes
+    let inferLevel ← shouldInferResultUniverse u
+    withUsed vars indTypes fun vars => do
+      let numVars   := vars.size
+      let numParams := numVars + numExplicitParams
+      let indTypes ← updateParams vars indTypes
+      let indTypes ← levelMVarToParam indTypes
+      let indTypes ← if inferLevel then updateResultingUniverse numParams indTypes else pure indTypes
+      let usedLevelNames := collectLevelParamsInInductive indTypes
       match sortDeclLevelParams scopeLevelNames allUserLevelNames usedLevelNames with
       | Except.error msg      => throwError msg
       | Except.ok levelParams => do
-        indTypes ← replaceIndFVarsWithConsts views indFVars levelParams numVars numParams indTypes;
-        let indTypes := applyInferMod views numParams indTypes;
-        let decl := Declaration.inductDecl levelParams numParams indTypes isUnsafe;
-        Term.ensureNoUnassignedMVars decl;
-        addDecl decl;
-        mkAuxConstructions views;
+        let indTypes ← replaceIndFVarsWithConsts views indFVars levelParams numVars numParams indTypes
+        let indTypes := applyInferMod views numParams indTypes
+        let decl := Declaration.inductDecl levelParams numParams indTypes isUnsafe
+        Term.ensureNoUnassignedMVars decl
+        addDecl decl
+        mkAuxConstructions views
         -- We need to invoke `applyAttributes` because `class` is implemented as an attribute.
-        views.forM fun view => Term.applyAttributesAt view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking
+        for view in views do
+          Term.applyAttributesAt view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking
 
 def elabInductiveViews (views : Array InductiveView) : CommandElabM Unit := do
-let view0 := views.get! 0;
-let ref := view0.ref;
-runTermElabM view0.declName fun vars => withRef ref $ mkInductiveDecl vars views
+let view0 := views[0]
+let ref := view0.ref
+runTermElabM view0.declName fun vars => withRef ref do
+  mkInductiveDecl vars views
 
-end Command
-end Elab
-end Lean
+end Lean.Elab.Command

stage0/src/Lean/Elab/StructInst.lean

@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -8,10 +9,7 @@ import Lean.Elab.App
 import Lean.Elab.Binders
 import Lean.Elab.Quotation
 
-namespace Lean
-namespace Elab
-namespace Term
-namespace StructInst
+namespace Lean.Elab.Term.StructInst
 
 open Std (HashMap)
 open Meta
@@ -20,12 +18,12 @@ open Meta
 
 @[builtinMacro Lean.Parser.Term.structInst] def expandStructInstExpectedType : Macro :=
 fun stx =>
-  let expectedArg := stx.getArg 4;
+  let expectedArg := stx[4]
   if expectedArg.isNone
     then Macro.throwUnsupported
   else
-    let expected := expectedArg.getArg 1;
-    let stxNew   := stx.setArg 4 mkNullNode;
+    let expected := expectedArg[1]
+    let stxNew   := stx.setArg 4 mkNullNode
     `(($stxNew : $expected))
 
 /-
@@ -34,17 +32,18 @@ If `stx` is of the form `{ s with ... }` and `s` is not a local variable, expand
 Note that this one is not a `Macro` because we need to access the local context.
 -/
 private def expandNonAtomicExplicitSource (stx : Syntax) : TermElabM (Option Syntax) :=
-withFreshMacroScope $
-  let sourceOpt := stx.getArg 1;
-  if sourceOpt.isNone then pure none  else do
-    let source := sourceOpt.getArg 0;
-    fvar? ← isLocalIdent? source;
-    match fvar? with
+withFreshMacroScope do
+  let sourceOpt := stx[1]
+  if sourceOpt.isNone then
+    pure none
+  else
+    let source := sourceOpt[0]
+    match (← isLocalIdent? source) with
     | some _ => pure none
-    | none   => do
-      src ← `(src);
-      let sourceOpt := sourceOpt.setArg 0 src;
-      let stxNew    := stx.setArg 1 sourceOpt;
+    | none   =>
+      let src ← `(src)
+      let sourceOpt := sourceOpt.setArg 0 src
+      let stxNew    := stx.setArg 1 sourceOpt
       `(let src := $source; $stxNew)
 
 inductive Source
@@ -64,15 +63,15 @@ def setStructSourceSyntax (structStx : Syntax) : Source → Syntax
 | Source.explicit stx _ => (structStx.setArg 1 stx).setArg 3 mkNullNode
 
 private def getStructSource (stx : Syntax) : TermElabM Source :=
-withRef stx $
-let explicitSource := stx.getArg 1;
-let implicitSource := stx.getArg 3;
+withRef stx do
+let explicitSource := stx[1]
+let implicitSource := stx[3]
 if explicitSource.isNone && implicitSource.isNone then
   pure Source.none
 else if explicitSource.isNone then
   pure $ Source.implicit implicitSource
-else if implicitSource.isNone then do
-  fvar? ← isLocalIdent? (explicitSource.getArg 0);
+else if implicitSource.isNone then
+  let fvar? ← isLocalIdent? explicitSource[0]
   match fvar? with
   | none      => unreachable! -- expandNonAtomicExplicitSource must have been used when we get here
   | some src  => pure $ Source.explicit explicitSource src
@@ -85,16 +84,16 @@ else
   def structInstArrayRef := parser! "[" >> termParser >>"]"
   ``` -/
 private def isModifyOp? (stx : Syntax) : TermElabM (Option Syntax) := do
-let args := (stx.getArg 2).getArgs;
-s? ← args.foldSepByM
+let args := stx[2].getArgs
+let s? ← args.foldSepByM
   (fun arg s? =>
     /- Remark: the syntax for `structInstField` is
        ```
        def structInstLVal   := (ident <|> numLit <|> structInstArrayRef) >> many (group ("." >> (ident <|> numLit)) <|> structInstArrayRef)
        def structInstField  := parser! structInstLVal >> " := " >> termParser
        ``` -/
-    let lval := arg.getArg 0;
-    let k    := lval.getKind;
+    let lval := arg[0]
+    let k    := lval.getKind
     if k == `Lean.Parser.Term.structInstArrayRef then
       match s? with
       | none   => pure (some arg)
@@ -111,56 +110,55 @@ s? ← args.foldSepByM
           throwErrorAt arg "invalid {...} notation, can't mix field and `[..]` at a given level"
         else
           pure s?)
-  none;
+  none
 match s? with
 | none   => pure none
-| some s => if (s.getArg 0).getKind == `Lean.Parser.Term.structInstArrayRef then pure s? else pure none
+| some s => if s[0].getKind == `Lean.Parser.Term.structInstArrayRef then pure s? else pure none
 
-private def elabModifyOp (stx modifyOp source : Syntax) (expectedType? : Option Expr) : TermElabM Expr :=
-let continue (val : Syntax) : TermElabM Expr := do {
-  let lval := modifyOp.getArg 0;
-  let idx  := lval.getArg 1;
-  let self := source.getArg 0;
-  stxNew ← `($(self).modifyOp (idx := $idx) (fun s => $val));
-  trace `Elab.struct.modifyOp fun _ => stx ++ "\n===>\n" ++ stxNew;
+private def elabModifyOp (stx modifyOp source : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
+let cont (val : Syntax) : TermElabM Expr := do
+  let lval := modifyOp[0]
+  let idx  := lval[1]
+  let self := source[0]
+  let stxNew ← `($(self).modifyOp (idx := $idx) (fun s => $val))
+  trace[Elab.struct.modifyOp]! "{stx}\n===>\n{stxNew}"
   withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
-}; do
-trace `Elab.struct.modifyOp fun _ => modifyOp ++ "\nSource: " ++ source;
-let rest := modifyOp.getArg 1;
-if rest.isNone then do
-  continue (modifyOp.getArg 3)
-else do
-  s ← `(s);
-  let valFirst  := rest.getArg 0;
-  let valFirst  := if valFirst.getKind == `Lean.Parser.Term.structInstArrayRef then valFirst else valFirst.getArg 1;
-  let restArgs  := rest.getArgs;
-  let valRest   := mkNullNode (restArgs.extract 1 restArgs.size);
-  let valField  := modifyOp.setArg 0 valFirst;
-  let valField  := valField.setArg 1 valRest;
-  let valSource := source.modifyArg 0 $ fun _ => s;
-  let val       := stx.setArg 1 valSource;
-  let val       := val.setArg 2 $ mkNullNode #[valField];
-  trace `Elab.struct.modifyOp fun _ => stx ++ "\nval: " ++ val;
-  continue val
+trace[Elab.struct.modifyOp]! "{modifyOp}\nSource: {source}"
+let rest := modifyOp[1]
+if rest.isNone then
+  cont modifyOp[3]
+else
+  let s ← `(s)
+  let valFirst  := rest[0]
+  let valFirst  := if valFirst.getKind == `Lean.Parser.Term.structInstArrayRef then valFirst else valFirst[1]
+  let restArgs  := rest.getArgs
+  let valRest   := mkNullNode restArgs[1:restArgs.size]
+  let valField  := modifyOp.setArg 0 valFirst
+  let valField  := valField.setArg 1 valRest
+  let valSource := source.modifyArg 0 fun _ => s
+  let val       := stx.setArg 1 valSource
+  let val       := val.setArg 2 $ mkNullNode #[valField]
+  trace[Elab.struct.modifyOp]! "{stx}\nval: {val}"
+  cont val
 
 /- Get structure name and elaborate explicit source (if available) -/
 private def getStructName (stx : Syntax) (expectedType? : Option Expr) (sourceView : Source) : TermElabM Name := do
-tryPostponeIfNoneOrMVar expectedType?;
+tryPostponeIfNoneOrMVar expectedType?
 let useSource : Unit → TermElabM Name := fun _ =>
   match sourceView, expectedType? with
   | Source.explicit _ src, _ => do
-    srcType ← inferType src;
-    srcType ← whnf srcType;
-    tryPostponeIfMVar srcType;
+    let srcType ← inferType src
+    let srcType ← whnf srcType
+    tryPostponeIfMVar srcType
     match srcType.getAppFn with
     | Expr.const constName _ _ => pure constName
-    | _ => throwError ("invalid {...} notation, source type is not of the form (C ...)" ++ indentExpr srcType)
-  | _, some expectedType => throwError ("invalid {...} notation, expected type is not of the form (C ...)" ++ indentExpr expectedType)
-  | _, none              => throwError ("invalid {...} notation, expected type must be known");
+    | _ => throwError! "invalid \{...} notation, source type is not of the form (C ...){indentExpr srcType}"
+  | _, some expectedType => throwError! "invalid \{...} notation, expected type is not of the form (C ...){indentExpr expectedType}"
+  | _, none              => throwError! "invalid \{...} notation, expected type must be known"
 match expectedType? with
 | none => useSource ()
-| some expectedType => do
-  expectedType ← whnf expectedType;
+| some expectedType =>
+  let expectedType ← whnf expectedType
   match expectedType.getAppFn with
   | Expr.const constName _ _ => pure constName
   | _                        => useSource ()
@@ -178,9 +176,9 @@ instance FieldLHS.hasFormat : HasFormat FieldLHS :=
   | FieldLHS.modifyOp _ i   => "[" ++ i.prettyPrint ++ "]"⟩
 
 inductive FieldVal (σ : Type)
-| term  (stx : Syntax) : FieldVal
-| nested (s : σ)       : FieldVal
-| default              : FieldVal -- mark that field must be synthesized using default value
+| term  (stx : Syntax) : FieldVal σ
+| nested (s : σ)       : FieldVal σ
+| default              : FieldVal σ -- mark that field must be synthesized using default value
 
 structure Field (σ : Type) :=
 (ref : Syntax) (lhs : List FieldLHS) (val : FieldVal σ) (expr? : Option Expr := none)
@@ -203,7 +201,7 @@ partial def Struct.allDefault : Struct → Bool
 | ⟨_, _, fields, _⟩ => fields.all fun ⟨_, _, val, _⟩ => match val with
   | FieldVal.term _   => false
   | FieldVal.default  => true
-  | FieldVal.nested s => Struct.allDefault s
+  | FieldVal.nested s => allDefault s
 
 def Struct.ref : Struct → Syntax
 | ⟨ref, _, _, _⟩ => ref
@@ -226,7 +224,7 @@ Format.joinSep field.lhs " . " ++ " := " ++
 
 partial def formatStruct : Struct → Format
 | ⟨_, structName, fields, source⟩ =>
-  let fieldsFmt := Format.joinSep (fields.map (formatField formatStruct)) ", ";
+  let fieldsFmt := Format.joinSep (fields.map (formatField formatStruct)) ", "
   match source with
   | Source.none           => "{" ++ fieldsFmt ++ "}"
   | Source.implicit _     => "{" ++ fieldsFmt ++ " .. }"
@@ -258,35 +256,34 @@ def FieldVal.toSyntax : FieldVal Struct → Syntax
 
 def Field.toSyntax : Field Struct → Syntax
 | field =>
-  let stx := field.ref;
-  let stx := stx.setArg 3 field.val.toSyntax;
+  let stx := field.ref
+  let stx := stx.setArg 3 field.val.toSyntax
   match field.lhs with
   | first::rest =>
-    let stx := stx.setArg 0 $ first.toSyntax true;
-    let stx := stx.setArg 1 $ mkNullNode $ rest.toArray.map (FieldLHS.toSyntax false);
+    let stx := stx.setArg 0 $ first.toSyntax true
+    let stx := stx.setArg 1 $ mkNullNode $ rest.toArray.map (FieldLHS.toSyntax false)
     stx
   | _ => unreachable!
 
 private def toFieldLHS (stx : Syntax) : Except String FieldLHS :=
 if stx.getKind == `Lean.Parser.Term.structInstArrayRef then
-  pure $ FieldLHS.modifyOp stx (stx.getArg 1)
+  pure $ FieldLHS.modifyOp stx stx[1]
 else
   -- Note that the representation of the first field is different.
-  let stx := if stx.getKind == nullKind then stx.getArg 1 else stx;
+  let stx := if stx.getKind == nullKind then stx[1] else stx
   if stx.isIdent then pure $ FieldLHS.fieldName stx stx.getId.eraseMacroScopes
   else match stx.isFieldIdx? with
     | some idx => pure $ FieldLHS.fieldIndex stx idx
     | none     => throw "unexpected structure syntax"
 
 private def mkStructView (stx : Syntax) (structName : Name) (source : Source) : Except String Struct := do
-let args      := (stx.getArg 2).getArgs;
-let fieldsStx := args.filter $ fun arg => arg.getKind == `Lean.Parser.Term.structInstField;
-fields ← fieldsStx.toList.mapM $ fun fieldStx => do {
-  let val   := fieldStx.getArg 3;
-  first ← toFieldLHS (fieldStx.getArg 0);
-  rest  ← (fieldStx.getArg 1).getArgs.toList.mapM toFieldLHS;
+let args      := stx[2].getArgs
+let fieldsStx := args.filter $ fun arg => arg.getKind == `Lean.Parser.Term.structInstField
+let fields ← fieldsStx.toList.mapM fun fieldStx => do
+  let val   := fieldStx[3]
+  let first ← toFieldLHS fieldStx[0]
+  let rest  ← fieldStx[1].getArgs.toList.mapM toFieldLHS
   pure $ ({ref := fieldStx, lhs := first :: rest, val := FieldVal.term val } : Field Struct)
-};
 pure ⟨stx, structName, fields, source⟩
 
 def Struct.modifyFieldsM {m : Type → Type} [Monad m] (s : Struct) (f : Fields → m Fields) : m Struct :=
@@ -297,25 +294,25 @@ match s with
 Id.run $ s.modifyFieldsM f
 
 def Struct.setFields (s : Struct) (fields : Fields) : Struct :=
-s.modifyFields $ fun _ => fields
+s.modifyFields fun _ => fields
 
 private def expandCompositeFields (s : Struct) : Struct :=
 s.modifyFields $ fun fields => fields.map $ fun field => match field with
   | { lhs := FieldLHS.fieldName ref (Name.str Name.anonymous _ _) :: rest, .. } => field
   | { lhs := FieldLHS.fieldName ref n@(Name.str _ _ _) :: rest, .. } =>
-    let newEntries := n.components.map $ FieldLHS.fieldName ref;
+    let newEntries := n.components.map $ FieldLHS.fieldName ref
     { field with lhs := newEntries ++ rest }
   | _ => field
 
 private def expandNumLitFields (s : Struct) : TermElabM Struct :=
-s.modifyFieldsM $ fun fields => do
-  env ← getEnv;
-  let fieldNames := getStructureFields env s.structName;
-  fields.mapM $ fun field => match field with
+s.modifyFieldsM fun fields => do
+  let env ← getEnv
+  let fieldNames := getStructureFields env s.structName
+  fields.mapM fun field => match field with
     | { lhs := FieldLHS.fieldIndex ref idx :: rest, .. } =>
       if idx == 0 then throwErrorAt ref "invalid field index, index must be greater than 0"
-      else if idx > fieldNames.size then throwErrorAt ref ("invalid field index, structure has only #" ++ toString fieldNames.size ++ " fields")
-      else pure { field with lhs := FieldLHS.fieldName ref (fieldNames.get! $ idx - 1) :: rest }
+      else if idx > fieldNames.size then throwErrorAt! ref "invalid field index, structure has only #{fieldNames.size} fields"
+      else pure { field with lhs := FieldLHS.fieldName ref fieldNames[idx - 1] :: rest }
     | _ => pure field
 
 /- For example, consider the following structures:
@@ -334,38 +331,36 @@ s.modifyFieldsM $ fun fields => do
    { toB.toA.x := 0, toB.y := 0, z := true : C }
    ``` -/
 private def expandParentFields (s : Struct) : TermElabM Struct := do
-env ← getEnv;
-s.modifyFieldsM $ fun fields => fields.mapM $ fun field => match field with
+let env ← getEnv
+s.modifyFieldsM fun fields => fields.mapM fun field => match field with
   | { lhs := FieldLHS.fieldName ref fieldName :: rest, .. } =>
     match findField? env s.structName fieldName with
-    | none => throwErrorAt ref ("'" ++ fieldName ++ "' is not a field of structure '" ++ s.structName ++ "'")
+    | none => throwErrorAt! ref "'{fieldName}' is not a field of structure '{s.structName}'"
     | some baseStructName =>
       if baseStructName == s.structName then pure field
       else match getPathToBaseStructure? env baseStructName s.structName with
         | some path => do
           let path := path.map $ fun funName => match funName with
             | Name.str _ s _ => FieldLHS.fieldName ref (mkNameSimple s)
-            | _              => unreachable!;
+            | _              => unreachable!
           pure { field with lhs := path ++ field.lhs }
-        | _ => throwErrorAt ref ("failed to access field '" ++ fieldName ++ "' in parent structure")
+        | _ => throwErrorAt! ref "failed to access field '{fieldName}' in parent structure"
   | _ => pure field
 
 private abbrev FieldMap := HashMap Name Fields
 
 private def mkFieldMap (fields : Fields) : TermElabM FieldMap :=
-fields.foldlM
-  (fun fieldMap field =>
-    match field.lhs with
-    | FieldLHS.fieldName _ fieldName :: rest =>
-      match fieldMap.find? fieldName with
-      | some (prevField::restFields) =>
-        if field.isSimple || prevField.isSimple then
-          throwErrorAt field.ref ("field '" ++ fieldName ++ "' has already beed specified")
-        else
-          pure $ fieldMap.insert fieldName (field::prevField::restFields)
-      | _ => pure $ fieldMap.insert fieldName [field]
-    | _ => unreachable!)
-  {}
+fields.foldlM (init := {}) fun fieldMap field =>
+  match field.lhs with
+  | FieldLHS.fieldName _ fieldName :: rest =>
+    match fieldMap.find? fieldName with
+    | some (prevField::restFields) =>
+      if field.isSimple || prevField.isSimple then
+        throwErrorAt! field.ref "field '{fieldName}' has already beed specified"
+      else
+        pure $ fieldMap.insert fieldName (field::prevField::restFields)
+    | _ => pure $ fieldMap.insert fieldName [field]
+  | _ => unreachable!
 
 private def isSimpleField? : Fields → Option (Field Struct)
 | [field] => if field.isSimple then some field else none
@@ -374,7 +369,7 @@ private def isSimpleField? : Fields → Option (Field Struct)
 private def getFieldIdx (structName : Name) (fieldNames : Array Name) (fieldName : Name) : TermElabM Nat := do
 match fieldNames.findIdx? $ fun n => n == fieldName with
 | some idx => pure idx
-| none     => throwError ("field '" ++ fieldName ++ "' is not a valid field of '" ++ structName ++ "'")
+| none     => throwError! "field '{fieldName}' is not a valid field of '{structName}'"
 
 private def mkProjStx (s : Syntax) (fieldName : Name) : Syntax :=
 Syntax.node `Lean.Parser.Term.proj #[s, mkAtomFrom s ".", mkIdentFrom s fieldName]
@@ -382,81 +377,78 @@ Syntax.node `Lean.Parser.Term.proj #[s, mkAtomFrom s ".", mkIdentFrom s fieldNam
 private def mkSubstructSource (structName : Name) (fieldNames : Array Name) (fieldName : Name) (src : Source) : TermElabM Source :=
 match src with
 | Source.explicit stx src => do
-  idx ← getFieldIdx structName fieldNames fieldName;
-  let stx := stx.modifyArg 0 $ fun stx => mkProjStx stx fieldName;
+  let idx ← getFieldIdx structName fieldNames fieldName
+  let stx := stx.modifyArg 0 fun stx => mkProjStx stx fieldName
   pure $ Source.explicit stx (mkProj structName idx src)
 | s => pure s
 
 @[specialize] private def groupFields (expandStruct : Struct → TermElabM Struct) (s : Struct) : TermElabM Struct := do
-env ← getEnv;
-let fieldNames := getStructureFields env s.structName;
-withRef s.ref $
-s.modifyFieldsM $ fun fields => do
-  fieldMap ← mkFieldMap fields;
-  fieldMap.toList.mapM $ fun ⟨fieldName, fields⟩ =>
+let env ← getEnv
+let fieldNames := getStructureFields env s.structName
+withRef s.ref do
+s.modifyFieldsM fun fields => do
+  let fieldMap ← mkFieldMap fields
+  fieldMap.toList.mapM fun ⟨fieldName, fields⟩ => do
     match isSimpleField? fields with
     | some field => pure field
-    | none => do
-      let substructFields := fields.map $ fun field => { field with lhs := field.lhs.tail! };
-      substructSource ← mkSubstructSource s.structName fieldNames fieldName s.source;
-      let field := fields.head!;
+    | none =>
+      let substructFields := fields.map fun field => { field with lhs := field.lhs.tail! }
+      let substructSource ← mkSubstructSource s.structName fieldNames fieldName s.source
+      let field := fields.head!
       match Lean.isSubobjectField? env s.structName fieldName with
-      | some substructName => do
-        let substruct := Struct.mk s.ref substructName substructFields substructSource;
-        substruct ← expandStruct substruct;
+      | some substructName =>
+        let substruct := Struct.mk s.ref substructName substructFields substructSource
+        let substruct ← expandStruct substruct
         pure { field with lhs := [field.lhs.head!], val := FieldVal.nested substruct }
       | none => do
         -- It is not a substructure field. Thus, we wrap fields using `Syntax`, and use `elabTerm` to process them.
-        let valStx := s.ref; -- construct substructure syntax using s.ref as template
-        let valStx := valStx.setArg 4 mkNullNode; -- erase optional expected type
-        let args   := substructFields.toArray.map $ Field.toSyntax;
-        let valStx := valStx.setArg 2 (mkSepStx args (mkAtomFrom s.ref ","));
-        let valStx := setStructSourceSyntax valStx substructSource;
+        let valStx := s.ref -- construct substructure syntax using s.ref as template
+        let valStx := valStx.setArg 4 mkNullNode -- erase optional expected type
+        let args   := substructFields.toArray.map Field.toSyntax
+        let valStx := valStx.setArg 2 (mkSepStx args (mkAtomFrom s.ref ","))
+        let valStx := setStructSourceSyntax valStx substructSource
         pure { field with lhs := [field.lhs.head!], val := FieldVal.term valStx }
 
 def findField? (fields : Fields) (fieldName : Name) : Option (Field Struct) :=
-fields.find? $ fun field =>
+fields.find? fun field =>
   match field.lhs with
   | [FieldLHS.fieldName _ n] => n == fieldName
   | _                        => false
 
 @[specialize] private def addMissingFields (expandStruct : Struct → TermElabM Struct) (s : Struct) : TermElabM Struct := do
-env ← getEnv;
-let fieldNames := getStructureFields env s.structName;
-let ref := s.ref;
+let env ← getEnv
+let fieldNames := getStructureFields env s.structName
+let ref := s.ref
 withRef ref do
-fields ← fieldNames.foldlM
-  (fun fields fieldName => do
-    match findField? s.fields fieldName with
-    | some field => pure $ field::fields
-    | none       =>
-      let addField (val : FieldVal Struct) : TermElabM Fields := do {
-        pure $ { ref := s.ref, lhs := [FieldLHS.fieldName s.ref fieldName], val := val } :: fields
-      };
-      match Lean.isSubobjectField? env s.structName fieldName with
-      | some substructName => do
-        substructSource ← mkSubstructSource s.structName fieldNames fieldName s.source;
-        let substruct := Struct.mk s.ref substructName [] substructSource;
-        substruct ← expandStruct substruct;
-        addField (FieldVal.nested substruct)
-      | none =>
-        match s.source with
-        | Source.none           => addField FieldVal.default
-        | Source.implicit _     => addField (FieldVal.term (mkHole s.ref))
-        | Source.explicit stx _ =>
-          -- stx is of the form `optional (try (termParser >> "with"))`
-          let src := stx.getArg 0;
-          let val := mkProjStx src fieldName;
-          addField (FieldVal.term val))
-  [];
+let fields ← fieldNames.foldlM (init := []) fun fields fieldName => do
+  match findField? s.fields fieldName with
+  | some field => pure $ field::fields
+  | none       =>
+    let addField (val : FieldVal Struct) : TermElabM Fields := do
+      pure $ { ref := s.ref, lhs := [FieldLHS.fieldName s.ref fieldName], val := val } :: fields
+    match Lean.isSubobjectField? env s.structName fieldName with
+    | some substructName => do
+      let substructSource ← mkSubstructSource s.structName fieldNames fieldName s.source
+      let substruct := Struct.mk s.ref substructName [] substructSource
+      let substruct ← expandStruct substruct
+      addField (FieldVal.nested substruct)
+    | none =>
+      match s.source with
+      | Source.none           => addField FieldVal.default
+      | Source.implicit _     => addField (FieldVal.term (mkHole s.ref))
+      | Source.explicit stx _ =>
+        -- stx is of the form `optional (try (termParser >> "with"))`
+        let src := stx[0]
+        let val := mkProjStx src fieldName
+        addField (FieldVal.term val)
 pure $ s.setFields fields.reverse
 
 private partial def expandStruct : Struct → TermElabM Struct
 | s => do
-  let s := expandCompositeFields s;
-  s ← expandNumLitFields s;
-  s ← expandParentFields s;
-  s ← groupFields expandStruct s;
+  let s := expandCompositeFields s
+  let s ← expandNumLitFields s
+  let s ← expandParentFields s
+  let s ← groupFields expandStruct s
   addMissingFields expandStruct s
 
 structure CtorHeaderResult :=
@@ -467,15 +459,15 @@ structure CtorHeaderResult :=
 private def mkCtorHeaderAux : Nat → Expr → Expr → Array MVarId → TermElabM CtorHeaderResult
 | 0,   type, ctorFn, instMVars => pure { ctorFn := ctorFn, ctorFnType := type, instMVars := instMVars }
 | n+1, type, ctorFn, instMVars => do
-  type ← whnfForall type;
+  let type ← whnfForall type
   match type with
   | Expr.forallE _ d b c =>
     match c.binderInfo with
-    | BinderInfo.instImplicit => do
-      a ← mkFreshExprMVar d MetavarKind.synthetic;
+    | BinderInfo.instImplicit =>
+      let a ← mkFreshExprMVar d MetavarKind.synthetic
       mkCtorHeaderAux n (b.instantiate1 a) (mkApp ctorFn a) (instMVars.push a.mvarId!)
-    | _ => do
-      a ← mkFreshExprMVar d;
+    | _ =>
+      let a ← mkFreshExprMVar d
       mkCtorHeaderAux n (b.instantiate1 a) (mkApp ctorFn a) instMVars
   | _ => throwError "unexpected constructor type"
 
@@ -487,21 +479,21 @@ private partial def getForallBody : Nat → Expr → Option Expr
 private def propagateExpectedType (type : Expr) (numFields : Nat) (expectedType? : Option Expr) : TermElabM Unit :=
 match expectedType? with
 | none              => pure ()
-| some expectedType =>
+| some expectedType => do
   match getForallBody numFields type with
     | none           => pure ()
     | some typeBody =>
-      unless typeBody.hasLooseBVars $ do
-        _ ← isDefEq expectedType typeBody;
+      unless typeBody.hasLooseBVars do
+        isDefEq expectedType typeBody
         pure ()
 
 private def mkCtorHeader (ctorVal : ConstructorVal) (expectedType? : Option Expr) : TermElabM CtorHeaderResult := do
-lvls ← ctorVal.lparams.mapM $ fun _ => mkFreshLevelMVar;
-let val  := Lean.mkConst ctorVal.name lvls;
-let type := (ConstantInfo.ctorInfo ctorVal).instantiateTypeLevelParams lvls;
-r ← mkCtorHeaderAux ctorVal.nparams type val #[];
-propagateExpectedType r.ctorFnType ctorVal.nfields expectedType?;
-synthesizeAppInstMVars r.instMVars;
+let lvls ← ctorVal.lparams.mapM fun _ => mkFreshLevelMVar
+let val  := Lean.mkConst ctorVal.name lvls
+let type := (ConstantInfo.ctorInfo ctorVal).instantiateTypeLevelParams lvls
+let r ← mkCtorHeaderAux ctorVal.nparams type val #[]
+propagateExpectedType r.ctorFnType ctorVal.nfields expectedType?
+synthesizeAppInstMVars r.instMVars
 pure r
 
 def markDefaultMissing (e : Expr) : Expr :=
@@ -511,43 +503,40 @@ def defaultMissing? (e : Expr) : Option Expr :=
 annotation? `structInstDefault e
 
 def throwFailedToElabField {α} (fieldName : Name) (structName : Name) (msgData : MessageData) : TermElabM α :=
-throwError ("failed to elaborate field '" ++ fieldName ++ "' of '" ++ structName ++ ", " ++ msgData)
+throwError! "failed to elaborate field '{fieldName}' of '{structName}, {msgData}"
 
-def trySynthStructInstance? (s : Struct) (expectedType : Expr) : TermElabM (Option Expr) :=
-if !s.allDefault then pure none
+def trySynthStructInstance? (s : Struct) (expectedType : Expr) : TermElabM (Option Expr) := do
+if !s.allDefault then
+  pure none
 else
-  catch (synthInstance? expectedType) (fun _ => pure none)
+  try synthInstance? expectedType catch _ => pure none
 
 private partial def elabStruct : Struct → Option Expr → TermElabM (Expr × Struct)
 | s, expectedType? => withRef s.ref do
-  env ← getEnv;
-  let ctorVal := getStructureCtor env s.structName;
-  { ctorFn := ctorFn, ctorFnType := ctorFnType, .. } ← mkCtorHeader ctorVal expectedType?;
-  (e, _, fields) ← s.fields.foldlM
-    (fun (acc : Expr × Expr × Fields) field =>
-      let (e, type, fields) := acc;
-      match field.lhs with
-      | [FieldLHS.fieldName ref fieldName] => do
-        type ← whnfForall type;
-        match type with
-        | Expr.forallE _ d b c =>
-          let continue (val : Expr) (field : Field Struct) : TermElabM (Expr × Expr × Fields) := do {
-            let e     := mkApp e val;
-            let type  := b.instantiate1 val;
-            let field := { field with expr? := some val };
-            pure (e, type, field::fields)
-          };
-          match field.val with
-          | FieldVal.term stx => do val ← elabTermEnsuringType stx d; continue val field
-          | FieldVal.nested s => do
-            val? ← trySynthStructInstance? s d; -- if all fields of `s` are marked as `default`, then try to synthesize instance
-            match val? with
-            | some val => continue val { field with val := FieldVal.term (mkHole field.ref) }
-            | none     => do(val, sNew) ← elabStruct s (some d); val ← ensureHasType d val; continue val { field with val := FieldVal.nested sNew }
-          | FieldVal.default  => do val ← withRef field.ref $ mkFreshExprMVar (some d); continue (markDefaultMissing val) field
-        | _ => withRef field.ref $ throwFailedToElabField fieldName s.structName ("unexpected constructor type" ++ indentExpr type)
-      | _ => throwErrorAt field.ref "unexpected unexpanded structure field")
-    (ctorFn, ctorFnType, []);
+  let env ← getEnv
+  let ctorVal := getStructureCtor env s.structName
+  let { ctorFn := ctorFn, ctorFnType := ctorFnType, .. } ← mkCtorHeader ctorVal expectedType?
+  let (e, _, fields) ← s.fields.foldlM (init := (ctorFn, ctorFnType, [])) fun (e, type, fields) field =>
+    match field.lhs with
+    | [FieldLHS.fieldName ref fieldName] => do
+      let type ← whnfForall type
+      match type with
+      | Expr.forallE _ d b c =>
+        let cont (val : Expr) (field : Field Struct) : TermElabM (Expr × Expr × Fields) := do
+          let e     := mkApp e val
+          let type  := b.instantiate1 val
+          let field := { field with expr? := some val }
+          pure (e, type, field::fields)
+        match field.val with
+        | FieldVal.term stx => cont (← elabTermEnsuringType stx d) field
+        | FieldVal.nested s => do
+          -- if all fields of `s` are marked as `default`, then try to synthesize instance
+          match (← trySynthStructInstance? s d) with
+          | some val => cont val { field with val := FieldVal.term (mkHole field.ref) }
+          | none     => do let (val, sNew) ← elabStruct s (some d); val ← ensureHasType d val; cont val { field with val := FieldVal.nested sNew }
+        | FieldVal.default  => do let val ← withRef field.ref $ mkFreshExprMVar (some d); cont (markDefaultMissing val) field
+      | _ => withRef field.ref $ throwFailedToElabField fieldName s.structName msg!"unexpected constructor type{indentExpr type}"
+    | _ => throwErrorAt field.ref "unexpected unexpanded structure field"
   pure (e, s.setFields fields.reverse)
 
 namespace DefaultFields
@@ -587,28 +576,24 @@ structure State :=
 
 partial def collectStructNames : Struct → Array Name → Array Name
 | struct, names =>
-  let names := names.push struct.structName;
-  struct.fields.foldl
-    (fun names field =>
-      match field.val with
-      | FieldVal.nested struct => collectStructNames struct names
-      | _ => names)
-    names
+  let names := names.push struct.structName
+  struct.fields.foldl (init := names) fun names field =>
+    match field.val with
+    | FieldVal.nested struct => collectStructNames struct names
+    | _ => names
 
 partial def getHierarchyDepth : Struct → Nat
 | struct =>
-  struct.fields.foldl
-    (fun max field =>
-      match field.val with
-      | FieldVal.nested struct => Nat.max max (getHierarchyDepth struct + 1)
-      | _ => max)
-    0
+  struct.fields.foldl (init := 0) fun max field =>
+    match field.val with
+    | FieldVal.nested struct => Nat.max max (getHierarchyDepth struct + 1)
+    | _ => max
 
 partial def findDefaultMissing? (mctx : MetavarContext) : Struct → Option (Field Struct)
 | struct =>
-  struct.fields.findSome? $ fun field =>
+  struct.fields.findSome? fun field =>
    match field.val with
-   | FieldVal.nested struct => findDefaultMissing? struct
+   | FieldVal.nested struct => findDefaultMissing? mctx struct
    | _ => match field.expr? with
      | none      => unreachable!
      | some expr => match defaultMissing? expr with
@@ -623,31 +608,30 @@ match field.lhs with
 abbrev M := ReaderT Context (StateRefT State TermElabM)
 
 def isRoundDone : M Bool := do
-ctx ← read;
-s ← get;
-pure (s.progress && ctx.maxDistance > 0)
+return (← get).progress && (← read).maxDistance > 0
 
 def getFieldValue? (struct : Struct) (fieldName : Name) : Option Expr :=
-struct.fields.findSome? $ fun field =>
+struct.fields.findSome? fun field =>
   if getFieldName field == fieldName then
     field.expr?
   else
     none
 
 partial def mkDefaultValueAux? (struct : Struct) : Expr → TermElabM (Option Expr)
-| Expr.lam n d b c => withRef struct.ref $
+| Expr.lam n d b c => withRef struct.ref do
   if c.binderInfo.isExplicit then
-    let fieldName := n;
+    let fieldName := n
     match getFieldValue? struct fieldName with
     | none     => pure none
-    | some val => do
-      valType ← inferType val;
-      condM (isDefEq valType d)
-        (mkDefaultValueAux? (b.instantiate1 val))
-        (pure none)
-  else do
-    arg ← mkFreshExprMVar d;
-    mkDefaultValueAux? (b.instantiate1 arg)
+    | some val =>
+      let valType ← inferType val
+      if (← isDefEq valType d) then
+        mkDefaultValueAux? struct (b.instantiate1 val)
+      else
+        pure none
+  else
+    let arg ← mkFreshExprMVar d
+    mkDefaultValueAux? struct (b.instantiate1 arg)
 | e =>
   if e.isAppOfArity `id 2 then
     pure (some e.appArg!)
@@ -656,7 +640,7 @@ partial def mkDefaultValueAux? (struct : Struct) : Expr → TermElabM (Option Ex
 
 def mkDefaultValue? (struct : Struct) (cinfo : ConstantInfo) : TermElabM (Option Expr) :=
 withRef struct.ref do
-us ← cinfo.lparams.mapM $ fun _ => mkFreshLevelMVar;
+let us ← cinfo.lparams.mapM fun _ => mkFreshLevelMVar
 mkDefaultValueAux? struct (cinfo.instantiateValueLevelParams us)
 
 /-- If `e` is a projection function of one of the given structures, then reduce it -/
@@ -664,7 +648,7 @@ def reduceProjOf? (structNames : Array Name) (e : Expr) : MetaM (Option Expr) :=
 if !e.isApp then pure none
 else match e.getAppFn with
   | Expr.const name _ _ => do
-    env ← getEnv;
+    let env ← getEnv
     match env.getProjectionStructureName? name with
     | some structName =>
       if structNames.contains structName then
@@ -676,142 +660,126 @@ else match e.getAppFn with
 
 /-- Reduce default value. It performs beta reduction and projections of the given structures. -/
 partial def reduce (structNames : Array Name) : Expr → MetaM Expr
-| e@(Expr.lam _ _ _ _)     => lambdaLetTelescope e $ fun xs b => do b ← reduce b; mkLambdaFVars xs b
-| e@(Expr.forallE _ _ _ _) => forallTelescope e $ fun xs b => do b ← reduce b; mkForallFVars xs b
-| e@(Expr.letE _ _ _ _ _)  => lambdaLetTelescope e $ fun xs b => do b ← reduce b; mkLetFVars xs b
+| e@(Expr.lam _ _ _ _)     => lambdaLetTelescope e fun xs b => do mkLambdaFVars xs (← reduce structNames b)
+| e@(Expr.forallE _ _ _ _) => forallTelescope e fun xs b => do mkForallFVars xs (← reduce structNames b)
+| e@(Expr.letE _ _ _ _ _)  => lambdaLetTelescope e fun xs b => do mkLetFVars xs (← reduce structNames b)
 | e@(Expr.proj _ i b _)    => do
-  r? ← Meta.reduceProj? b i;
-  match r? with
-  | some r => reduce r
-  | none   => do b ← reduce b; pure $ e.updateProj! b
+  match (← Meta.reduceProj? b i) with
+  | some r => reduce structNames r
+  | none   => pure $ e.updateProj! (← reduce structNames b)
 | e@(Expr.app f _ _) => do
-  r? ← reduceProjOf? structNames e;
-  match r? with
-  | some r => reduce r
-  | none   => do
-    let f := f.getAppFn;
-    f' ← reduce f;
+  match (← reduceProjOf? structNames e) with
+  | some r => reduce structNames r
+  | none   =>
+    let f := f.getAppFn
+    let f' ← reduce structNames f
     if f'.isLambda then
-      let revArgs := e.getAppRevArgs;
-      reduce $ f'.betaRev revArgs
-    else do
-      args ← e.getAppArgs.mapM reduce;
+      let revArgs := e.getAppRevArgs
+      reduce structNames (f'.betaRev revArgs)
+    else
+      let args ← e.getAppArgs.mapM (reduce structNames)
       pure (mkAppN f' args)
 | e@(Expr.mdata _ b _) => do
-  b ← reduce b;
+  let b ← reduce structNames b
   if (defaultMissing? e).isSome && !b.isMVar then
     pure b
   else
     pure $ e.updateMData! b
 | e@(Expr.mvar mvarId _) => do
-  val? ← getExprMVarAssignment? mvarId;
-  match val? with
-  | some val => if val.isMVar then reduce val else pure val
+  match (← getExprMVarAssignment? mvarId) with
+  | some val => if val.isMVar then reduce structNames val else pure val
   | none     => pure e
 | e => pure e
 
-partial def tryToSynthesizeDefaultAux (structs : Array Struct) (allStructNames : Array Name) (maxDistance : Nat)
-    (fieldName : Name) (mvarId : MVarId) : Nat → Nat → TermElabM Bool
-| i, dist =>
-  if dist > maxDistance then pure false
+partial def tryToSynthesizeDefault (structs : Array Struct) (allStructNames : Array Name) (maxDistance : Nat) (fieldName : Name) (mvarId : MVarId) : TermElabM Bool :=
+let rec loop (i : Nat) (dist : Nat) := do
+  if dist > maxDistance then
+    pure false
   else if h : i < structs.size then do
-    let struct := structs.get ⟨i, h⟩;
-    let defaultName := struct.structName ++ fieldName ++ `_default;
-    env ← getEnv;
+    let struct := structs.get ⟨i, h⟩
+    let defaultName := struct.structName ++ fieldName ++ `_default
+    let env ← getEnv
     match env.find? defaultName with
     | some cinfo@(ConstantInfo.defnInfo defVal) => do
-      mctx ← getMCtx;
-      val? ← mkDefaultValue? struct cinfo;
+      let mctx ← getMCtx
+      let val? ← mkDefaultValue? struct cinfo
       match val? with
-      | none     => do setMCtx mctx; tryToSynthesizeDefaultAux (i+1) (dist+1)
+      | none     => do setMCtx mctx; loop (i+1) (dist+1)
       | some val => do
-        val ← liftMetaM $ reduce allStructNames val;
-        match val.find? $ fun e => (defaultMissing? e).isSome with
-        | some _ => do setMCtx mctx; tryToSynthesizeDefaultAux (i+1) (dist+1)
-        | none   => do
-          mvarDecl ← getMVarDecl mvarId;
-          val ← ensureHasType mvarDecl.type val;
-          assignExprMVar mvarId val;
+        let val ← liftMetaM $ reduce allStructNames val
+        match val.find? fun e => (defaultMissing? e).isSome with
+        | some _ => setMCtx mctx; loop (i+1) (dist+1)
+        | none   =>
+          let mvarDecl ← getMVarDecl mvarId
+          let val ← ensureHasType mvarDecl.type val
+          assignExprMVar mvarId val
           pure true
-    | _ => tryToSynthesizeDefaultAux (i+1) dist
+    | _ => loop (i+1) dist
   else
     pure false
-
-def tryToSynthesizeDefault (structs : Array Struct) (allStructNames : Array Name)
-    (maxDistance : Nat) (fieldName : Name) (mvarId : MVarId) : TermElabM Bool :=
-tryToSynthesizeDefaultAux structs allStructNames maxDistance fieldName mvarId 0 0
+loop 0 0
 
 partial def step : Struct → M Unit
-| struct => unlessM isRoundDone $ withReader (fun ctx => { ctx with structs := ctx.structs.push struct }) $ do
-  struct.fields.forM $ fun field =>
+| struct => unlessM isRoundDone $ withReader (fun ctx => { ctx with structs := ctx.structs.push struct }) do
+  struct.fields.forM fun field => do
     match field.val with
     | FieldVal.nested struct => step struct
     | _ => match field.expr? with
       | none      => unreachable!
       | some expr => match defaultMissing? expr with
         | some (Expr.mvar mvarId _) =>
-          unlessM (liftM $ isExprMVarAssigned mvarId) $ do
-            ctx ← read;
-            whenM (liftM $ withRef field.ref $ tryToSynthesizeDefault ctx.structs ctx.allStructNames ctx.maxDistance (getFieldName field) mvarId) $ do
-              modify $ fun s => { s with progress := true }
+          unless (← isExprMVarAssigned mvarId) do
+            let ctx ← read
+            if (← withRef field.ref $ tryToSynthesizeDefault ctx.structs ctx.allStructNames ctx.maxDistance (getFieldName field) mvarId) then
+              modify fun s => { s with progress := true }
         | _ => pure ()
 
 partial def propagateLoop (hierarchyDepth : Nat) : Nat → Struct → M Unit
 | d, struct => do
-  mctx ← getMCtx;
-  match findDefaultMissing? mctx struct with
+  match findDefaultMissing? (← getMCtx) struct with
   | none       => pure () -- Done
   | some field =>
     if d > hierarchyDepth then
-      throwErrorAt field.ref ("field '" ++ getFieldName field ++ "' is missing")
-    else withReader (fun ctx => { ctx with maxDistance := d }) $ do
-      modify $ fun (s : State) => { s with progress := false };
-      step struct;
-      s ← get;
-      if s.progress then do
-        propagateLoop 0 struct
+      throwErrorAt! field.ref "field '{getFieldName field}' is missing"
+    else withReader (fun ctx => { ctx with maxDistance := d }) do
+      modify fun s => { s with progress := false }
+      step struct
+      if (← get).progress then do
+        propagateLoop hierarchyDepth 0 struct
       else
-        propagateLoop (d+1) struct
+        propagateLoop hierarchyDepth (d+1) struct
 
 def propagate (struct : Struct) : TermElabM Unit :=
-let hierarchyDepth := getHierarchyDepth struct;
-let structNames := collectStructNames struct #[];
+let hierarchyDepth := getHierarchyDepth struct
+let structNames := collectStructNames struct #[]
 (propagateLoop hierarchyDepth 0 struct { allStructNames := structNames }).run' {}
 
 end DefaultFields
 
 private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (source : Source) : TermElabM Expr := do
-structName ← getStructName stx expectedType? source;
-env ← getEnv;
-unless (isStructureLike env structName) $
-  throwError ("invalid {...} notation, '" ++ structName ++ "' is not a structure");
+let structName ← getStructName stx expectedType? source
+unless isStructureLike (← getEnv) structName do
+  throwError! "invalid \{...} notation, '{structName}' is not a structure"
 match mkStructView stx structName source with
 | Except.error ex  => throwError ex
-| Except.ok struct => do
-  struct ← expandStruct struct;
-  trace `Elab.struct fun _ => toString struct;
-  (r, struct) ← elabStruct struct expectedType?;
-  DefaultFields.propagate struct;
+| Except.ok struct =>
+  let struct ← expandStruct struct
+  trace[Elab.struct]! "{struct}"
+  let (r, struct) ← elabStruct struct expectedType?
+  DefaultFields.propagate struct
   pure r
 
 @[builtinTermElab structInst] def elabStructInst : TermElab :=
 fun stx expectedType? => do
-  stxNew? ← expandNonAtomicExplicitSource stx;
-  match stxNew? with
+  match (← expandNonAtomicExplicitSource stx) with
   | some stxNew => withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
-  | none => do
-    sourceView ← getStructSource stx;
-    modifyOp?  ← isModifyOp? stx;
-    match modifyOp?, sourceView with
+  | none =>
+    let sourceView ← getStructSource stx
+    match (← isModifyOp? stx), sourceView with
     | some modifyOp, Source.explicit source _ => elabModifyOp stx modifyOp source expectedType?
-    | some _,        _                        => throwError ("invalid {...} notation, explicit source is required when using '[<index>] := <value>'")
+    | some _,        _                        => throwError "invalid {...} notation, explicit source is required when using '[<index>] := <value>'"
     | _,             _                        => elabStructInstAux stx expectedType? sourceView
 
-@[init] private def regTraceClasses : IO Unit := do
-registerTraceClass `Elab.struct;
-pure ()
+initialize registerTraceClass `Elab.struct
 
-end StructInst
-end Term
-end Elab
-end Lean
+end Lean.Elab.Term.StructInst

stage0/src/Std/Data/HashMap.lean

@@ -168,13 +168,13 @@ self.find? idx
 match m with
 | ⟨ m, _ ⟩ => m.contains a
 
-@[inline] def foldM {δ : Type w} {m : Type w → Type w} [Monad m] (f : δ → α → β → m δ) (d : δ) (h : HashMap α β) : m δ :=
+@[inline] def foldM {δ : Type w} {m : Type w → Type w} [Monad m] (f : δ → α → β → m δ) (init : δ) (h : HashMap α β) : m δ :=
 match h with
-| ⟨ h, _ ⟩ => h.foldM f d
+| ⟨ h, _ ⟩ => h.foldM f init
 
-@[inline] def fold {δ : Type w} (f : δ → α → β → δ) (d : δ) (m : HashMap α β) : δ :=
+@[inline] def fold {δ : Type w} (f : δ → α → β → δ) (init : δ) (m : HashMap α β) : δ :=
 match m with
-| ⟨ m, _ ⟩ => m.fold f d
+| ⟨ m, _ ⟩ => m.fold f init
 
 @[inline] def size (m : HashMap α β) : Nat :=
 match m with

stage0/stdlib/Lean/Elab/Declaration.c

@@ -129,7 +129,6 @@ lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_expandMutualNamespa
 lean_object* l_Lean_Elab_Command_expandDeclNamespace_x3f_match__3___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__1___lambda__2___closed__3;
 lean_object* lean_array_fget(lean_object*, lean_object*);
-lean_object* l_Lean_Elab_applyVisibility___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_expandInitialize___closed__6;
 lean_object* l_Lean_Elab_Command_expandMutualPreamble_match__1___rarg(lean_object*, lean_object*, lean_object*);
@@ -272,6 +271,7 @@ lean_object* l___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyn
 lean_object* l_Lean_Syntax_getArgs(lean_object*);
 lean_object* l_Lean_Syntax_getKind(lean_object*);
 lean_object* l_Lean_MacroScopesView_review(lean_object*);
+lean_object* l_Lean_Elab_applyVisibility___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__7(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_applyAttributes(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_expandDeclNamespace_x3f___closed__4;
 lean_object* l_Lean_Elab_Command_expandMutualPreamble___closed__5;
@@ -2298,7 +2298,7 @@ lean_object* x_20; lean_object* x_21;
 x_20 = lean_ctor_get(x_5, 6);
 lean_dec(x_20);
 lean_ctor_set(x_5, 6, x_18);
-x_21 = l_Lean_Elab_applyVisibility___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8(x_14, x_12, x_5, x_6, x_17);
+x_21 = l_Lean_Elab_applyVisibility___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__7(x_14, x_12, x_5, x_6, x_17);
 if (lean_obj_tag(x_21) == 0)
 {
 uint8_t x_22; 
@@ -2463,7 +2463,7 @@ lean_ctor_set(x_66, 3, x_63);
 lean_ctor_set(x_66, 4, x_64);
 lean_ctor_set(x_66, 5, x_65);
 lean_ctor_set(x_66, 6, x_18);
-x_67 = l_Lean_Elab_applyVisibility___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8(x_14, x_12, x_66, x_6, x_17);
+x_67 = l_Lean_Elab_applyVisibility___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__7(x_14, x_12, x_66, x_6, x_17);
 if (lean_obj_tag(x_67) == 0)
 {
 lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; uint8_t x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; 

stage0/stdlib/Lean/Elab/Structure.c

@@ -15,12 +15,10 @@ extern "C" {
 #endif
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__2___lambda__2___closed__3;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectLevelParamsInFVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__7(lean_object*);
 extern lean_object* l_Lean_mkHole___closed__3;
 lean_object* l_Lean_Elab_Command_elabStructure___closed__11;
 lean_object* l_Lean_Meta_withLCtx___at_Lean_Elab_Term_elabBinders___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields___rarg___closed__12;
-lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabStructure___lambda__1___boxed(lean_object**);
 lean_object* l_Lean_Elab_Term_removeUnused(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_getResultUniverse___closed__1;
@@ -52,7 +50,6 @@ lean_object* lean_array_uget(lean_object*, size_t);
 lean_object* lean_io_error_to_string(lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withUsed___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_checkValidFieldModifier___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__7___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabStructure___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, 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* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__2___lambda__3___closed__3;
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__10(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -60,7 +57,6 @@ lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_levelMVarToPar
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__9(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Elab_Modifiers_isProtected(lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabFieldTypeValue_match__2___rarg(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_setEnv___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withParents___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_instantiateMVars___at_Lean_Elab_Term_declareTacticSyntax___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_name_eq(lean_object*, lean_object*);
@@ -76,6 +72,7 @@ lean_object* l_Lean_Meta_addGlobalInstance___at___private_Lean_Elab_Structure_0_
 lean_object* lean_array_fswap(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__2(lean_object*, lean_object*, lean_object*, uint8_t, 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_addDefaults(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__1(lean_object*, lean_object*, uint8_t, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Array_empty___closed__1;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields_match__5(lean_object*);
@@ -98,13 +95,12 @@ lean_object* l_Lean_Elab_Command_checkValidFieldModifier___lambda__1___closed__1
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields___rarg___closed__9;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__5(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_Term_ensureNoUnassignedMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Meta_getLevel___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, 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__8(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_getResultUniverse_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_elabModifiers___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__1___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_elabModifiers___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* lean_expr_instantiate1(lean_object*, lean_object*);
 lean_object* lean_array_push(lean_object*, lean_object*);
-lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
 uint8_t l_Lean_isInternalSubobjectFieldName(lean_object*);
 lean_object* lean_string_append(lean_object*, lean_object*);
@@ -116,18 +112,18 @@ lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addProjections
 lean_object* l_Lean_Elab_Term_applyAttributesAt(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_string_utf8_extract(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_getAppFn___main(lean_object*);
-extern lean_object* l___private_Lean_Elab_Inductive_26__removeUnused___closed__1;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_addMessageContextPartial___at_Lean_Elab_Command_Lean_AddMessageContext___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_validStructType_match__1(lean_object*);
 lean_object* l___private_Lean_Meta_InferType_4__getLevelImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_elabAttr___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__4___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_assignLevelMVar___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_updateResultingUniverse___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l___regBuiltin_Lean_Elab_Term_elabTypeStx___closed__2;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_mkAuxConstructions(lean_object*, lean_object*, lean_object*, lean_object*, 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__8___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___closed__1;
 lean_object* l_Lean_Elab_Command_shouldInferResultUniverse(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_getLevelNames___rarg(lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Command_accLevelAtCtor(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addCtorFields_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_string_utf8_byte_size(lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__2___closed__3;
@@ -141,12 +137,14 @@ lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Le
 lean_object* l_Array_forMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUsed___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withParents_match__1(lean_object*, lean_object*);
 uint8_t l_USize_decLt(size_t, size_t);
-lean_object* l_Lean_Meta_setMCtx___at___private_Lean_Meta_Basic_6__liftMkBindingM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___closed__2;
+lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___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*, lean_object*);
 lean_object* l_Lean_Elab_Command_checkValidFieldModifier___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l___private_Lean_Meta_Basic_1__regTraceClasses___closed__2;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addCtorFields___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_applyVisibility___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields___rarg___closed__2;
+lean_object* l_Lean_setEnv___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_checkValidFieldModifier___lambda__3___closed__1;
 lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addProjections___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -160,19 +158,18 @@ lean_object* l_Lean_Elab_Command_checkValidFieldModifier___lambda__4(lean_object
 lean_object* l___private_Lean_Meta_Closure_1__mkAuxDefinitionImp(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_logDbgTrace___rarg___closed__1;
 lean_object* l_Lean_Elab_Command_elabStructure___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, 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* l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5(lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_levelMVarToParamAux(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___private_Lean_Elab_Structure_0__Lean_Elab_Command_validStructType___boxed(lean_object*);
 lean_object* l_Lean_Elab_Command_StructFieldInfo_isFromParent___boxed(lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_updateResultingUniverse_match__1(lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_checkParentIsStructure___closed__2;
 uint8_t l_Lean_Elab_Command_StructFieldInfo_inferMod___default;
-lean_object* l_Lean_Meta_getLevel___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_elabModifiers___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields___rarg___closed__8;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_checkParentIsStructure___closed__4;
 lean_object* l_Lean_Elab_Command_checkValidFieldModifier___lambda__3___closed__2;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_processSubfields_loop(lean_object*);
+lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___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*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addCtorFields(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_elabModifiers___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__1___lambda__1___boxed(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_removeUnused_match__1___rarg(lean_object*, lean_object*);
@@ -185,12 +182,10 @@ lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_updateResultin
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabTermEnsuringType(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_fget(lean_object*, lean_object*);
-lean_object* l_Lean_Elab_applyVisibility___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields___rarg___closed__1;
 extern lean_object* l_Lean_Expr_Inhabited___closed__1;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_checkParentIsStructure___closed__1;
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
-lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__6___boxed(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_processSubfields_loop___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l___private_Lean_Elab_Structure_0__Lean_Elab_Command_validStructType(lean_object*);
 lean_object* lean_st_ref_take(lean_object*, lean_object*);
@@ -200,11 +195,9 @@ lean_object* l_Lean_Elab_Command_StructFieldInfo_isSubobject_match__1___rarg___b
 lean_object* l_Lean_Elab_elabDeclAttrs___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Elab_Command_StructFieldInfo_isSubobject(lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withParents___rarg___lambda__3(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*);
-lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_nat_sub(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabFieldTypeValue_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkProjection___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_processSubfields_loop___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_MetavarContext_instantiateLevelMVars___main(lean_object*, lean_object*);
 lean_object* l_Lean_addDecl___at_Lean_Elab_Term_declareTacticSyntax___spec__2(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_mkProjections___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_removeUnused_match__1(lean_object*);
@@ -216,6 +209,7 @@ lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withUsed_match
 lean_object* l_Array_shrink___main___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_inferType___at_Lean_Elab_Term_collectUsedFVarsAtFVars___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_getStructureFieldsFlattened(lean_object*, lean_object*);
+lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_expandDeclId(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabStructure___closed__8;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -223,7 +217,6 @@ lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Le
 extern lean_object* l_Lean_Expr_heq_x3f___closed__2;
 lean_object* l_List_map___main___at_Lean_Meta_addGlobalInstanceImp___spec__1(lean_object*);
 lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_checkParentIsStructure_match__1(lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -240,6 +233,7 @@ lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView(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_expandCtor___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabStructure___closed__4;
+extern lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_collectLevelParamsInInductive___closed__1;
 lean_object* l_Lean_Elab_elabAttr___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__4___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields_match__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields_match__2___rarg(lean_object*, lean_object*);
@@ -249,9 +243,9 @@ lean_object* l___private_Lean_Meta_AppBuilder_25__mkProjectionImp___main(lean_ob
 lean_object* l_Lean_Meta_mkProjection___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_processSubfields_loop___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_filterAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__7(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_filterAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__1(lean_object*, lean_object*, lean_object*);
+extern lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_removeUnused___closed__1;
 lean_object* l_Lean_Elab_Command_elabStructure___lambda__3(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_StructFieldInfo_value_x3f___default;
-lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_LocalDecl_binderInfo(lean_object*);
 extern lean_object* l_Lean_Meta_inferTypeRef;
 extern lean_object* l_Lean_Elab_elabModifiers___rarg___lambda__3___closed__2;
@@ -260,8 +254,10 @@ lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_getResultUnive
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addCtorFields_match__1(lean_object*);
 lean_object* l_Lean_Meta_mkId___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_addDefaults___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getId(lean_object*);
+lean_object* l_Lean_Meta_instantiateLevelMVars___at_Lean_Elab_Command_shouldInferResultUniverse___spec__1(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_processSubfields_loop___rarg___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*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_map___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4(lean_object*);
+lean_object* l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__2___closed__7;
 lean_object* l_Lean_Elab_Command_checkValidFieldModifier___lambda__1___closed__3;
@@ -276,7 +272,6 @@ lean_object* l_Lean_Elab_Command_StructFieldInfo_isSubobject___boxed(lean_object
 lean_object* l_Array_forMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_addDefaults___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectLevelParamsInStructure___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_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectLevelParamsInFVars___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_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Environment_contains(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_elabAttr___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__4___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__2___closed__2;
@@ -288,6 +283,7 @@ lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___b
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__2___lambda__2(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_checkValidFieldModifier___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withParents___rarg___closed__1;
+lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___closed__1;
 lean_object* l_Lean_Meta_getLocalInstances___at_Lean_Elab_Term_removeUnused___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabStructure___closed__5;
@@ -307,8 +303,8 @@ lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields___r
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__2___lambda__2___closed__1;
 lean_object* l_Lean_Elab_Command_elabStructure___closed__3;
 lean_object* l_Lean_Elab_sortDeclLevelParams(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Command_accLevelAtCtor___main(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_forMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUsed___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_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__6(lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__2___closed__8;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields_match__1___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkLambdaFVars___at_Lean_Elab_Term_elabFun___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -316,13 +312,11 @@ lean_object* l_Lean_Elab_Term_collectUsedFVars(lean_object*, lean_object*, lean_
 uint8_t l_Lean_BinderInfo_isInstImplicit(uint8_t);
 lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Array_append___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l___private_Lean_Elab_Inductive_34__mkAuxConstructions___closed__2;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_processSubfields_loop___rarg___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*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__2___closed__1;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___closed__3;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_processSubfields(lean_object*);
 extern lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
-lean_object* l_Lean_Meta_instantiateLevelMVars___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Meta_forallTelescopeCompatibleAux___rarg___lambda__3___closed__3;
 size_t lean_usize_of_nat(lean_object*);
 extern lean_object* l_Lean_registerClassAttr___closed__2;
@@ -331,7 +325,6 @@ lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_Structure_0__Lean_
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__2___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_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__2___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_LocalContext_updateBinderInfo(lean_object*, lean_object*, uint8_t);
-lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__2___boxed(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_collectLevelParamsInStructure___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addProjections(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -369,7 +362,6 @@ lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Le
 lean_object* l_Lean_Elab_elabAttr___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_forMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUsed___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___private_Lean_Elab_Structure_0__Lean_Elab_Command_getResultUniverse___closed__2;
-extern lean_object* l___private_Lean_Elab_Inductive_29__collectLevelParamsInInductive___closed__1;
 lean_object* l_Lean_Syntax_getSepArgs(lean_object*);
 uint8_t l_Lean_isAttribute(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabStructure___closed__6;
@@ -378,6 +370,7 @@ uint8_t l_Lean_BinderInfo_beq(uint8_t, uint8_t);
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__2___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getNumArgs(lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__2___lambda__3___closed__1;
+extern lean_object* l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkAuxConstructions___closed__2;
 lean_object* l_Lean_Elab_Command_elabStructure___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_processSubfields_loop___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_elabAttr___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__4___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -387,7 +380,6 @@ lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields_mat
 lean_object* l_Lean_Elab_Command_getCurrMacroScope(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_SourceInfo_inhabited___closed__1;
 lean_object* l_Lean_mkPrivateName(lean_object*, lean_object*);
-lean_object* l_Lean_Elab_addMacroStack___at_Lean_Elab_Command_Lean_AddErrorMessageContext___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l___private_Lean_Meta_AppBuilder_25__mkProjectionImp___main___closed__5;
 lean_object* l_Lean_Syntax_getArgs(lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__1___closed__1;
@@ -395,10 +387,10 @@ lean_object* l_Lean_Elab_Command_elabStructure___closed__2;
 lean_object* l_Lean_Elab_elabAttr___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__4___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getKind(lean_object*);
 lean_object* l_Array_forMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_levelMVarToParamFVars___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_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__6(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__2___closed__6;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___lambda__1(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__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_Elab_applyVisibility___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__7(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_elabAttr___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__4___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_processSubfields_loop___rarg___closed__2;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectLevelParamsInFVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -419,7 +411,6 @@ lean_object* l_Lean_Elab_Command_checkValidFieldModifier___lambda__3___closed__3
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_getResultUniverse___closed__3;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_addCtorFields_match__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Meta_instantiateLevelMVars___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__2___boxed(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_withFields___rarg___closed__6;
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__1___closed__3;
 lean_object* l_Lean_Elab_Command_getMainModule___rarg(lean_object*, lean_object*);
@@ -429,10 +420,10 @@ lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUsed_ma
 lean_object* l_Lean_Elab_Command_checkValidFieldModifier___lambda__4___closed__2;
 lean_object* l_Lean_MonadTracer_trace___at_Lean_Meta_isLevelDefEq___spec__2(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_withUsed___rarg___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_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__6___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_findMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_findFieldInfo_x3f___spec__1(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields_match__1(lean_object*);
 lean_object* l_Lean_Elab_Command_getRef(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_expandDeclSig(lean_object*);
 lean_object* l_Lean_Elab_Command_checkValidFieldModifier___closed__2;
 extern lean_object* l_Lean_ResolveName_resolveNamespaceUsingScope___closed__3;
@@ -477,17 +468,14 @@ lean_object* l_Lean_Elab_Command_checkValidFieldModifier___lambda__1(lean_object
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_updateResultingUniverse___closed__1;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___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*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_mkAuxConstructions___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__7___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_checkValidFieldModifier___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_checkValidFieldModifier___closed__1;
 uint8_t l_Lean_Elab_Modifiers_isPrivate(lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_findFieldInfo_x3f___boxed(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__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* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabStructure_match__1___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Name_appendBefore(lean_object*, lean_object*);
-lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_mkOptionalNode___closed__2;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_updateResultingUniverse___boxed(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_updateResultingUniverse___closed__2;
@@ -497,6 +485,7 @@ lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields_m
 lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__8___closed__1;
 lean_object* l_Lean_Meta_mkAuxDefinition___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_addDefaults___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_forMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_levelMVarToParamFVars___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_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__6___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_checkValidCtorModifier(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_levelMVarToParamFVar___boxed(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_expandCtor___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -513,6 +502,7 @@ lean_object* l_Lean_Level_mkNaryMax___main(lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withUsed_match__1___rarg(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_levelMVarToParamFVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkAuxDefinition___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_addDefaults___spec__2___closed__1;
+lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___lambda__2___closed__1;
 extern lean_object* l_Lean_Elab_elabAttr___rarg___lambda__3___closed__2;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabFieldTypeValue___closed__1;
@@ -528,6 +518,7 @@ lean_object* l_Lean_Elab_Command_checkValidInductiveModifier(lean_object*, lean_
 lean_object* l_Lean_mkConst(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_elabModifiers___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_processSubfields_loop___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_setEnv___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_CollectLevelParams_main___main(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkForallFVars___at_Lean_Elab_Term_elabForall___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withLocalDecl___at_Lean_Elab_Term_elabLetDeclAux___spec__3___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -538,9 +529,10 @@ lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabFieldTypeV
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_checkParentIsStructure_match__1___rarg(lean_object*, lean_object*, lean_object*);
 uint8_t lean_is_class(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___lambda__2___closed__3;
+lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Util_2__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_applyVisibility___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabStructure___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* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_elabModifiers___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__1___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_isStructure(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_elabAttrs___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -548,11 +540,9 @@ extern lean_object* l_Lean_Elab_checkNotAlreadyDeclared___rarg___lambda__1___clo
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields___rarg___closed__7;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_levelMVarToParam___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_getBetterRef(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields_match__4___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabFieldTypeValue(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_setEnv___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__10(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUsed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_defaultCtorName___closed__1;
 lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_mkCtor___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -763,68 +753,6 @@ x_1 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_defaultCtorName___clo
 return x_1;
 }
 }
-lean_object* l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(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 = l_Lean_Elab_Command_getRef(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_ctor_get(x_2, 4);
-lean_inc(x_8);
-lean_inc(x_8);
-x_9 = l_Lean_Elab_getBetterRef(x_6, x_8);
-lean_dec(x_6);
-x_10 = l_Lean_addMessageContextPartial___at_Lean_Elab_Command_Lean_AddMessageContext___spec__1(x_1, x_2, x_3, x_7);
-x_11 = lean_ctor_get(x_10, 0);
-lean_inc(x_11);
-x_12 = lean_ctor_get(x_10, 1);
-lean_inc(x_12);
-lean_dec(x_10);
-x_13 = l_Lean_Elab_addMacroStack___at_Lean_Elab_Command_Lean_AddErrorMessageContext___spec__1(x_11, x_8, x_2, x_3, x_12);
-lean_dec(x_2);
-lean_dec(x_8);
-x_14 = !lean_is_exclusive(x_13);
-if (x_14 == 0)
-{
-lean_object* x_15; lean_object* x_16; 
-x_15 = lean_ctor_get(x_13, 0);
-x_16 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_16, 0, x_9);
-lean_ctor_set(x_16, 1, x_15);
-lean_ctor_set_tag(x_13, 1);
-lean_ctor_set(x_13, 0, x_16);
-return x_13;
-}
-else
-{
-lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; 
-x_17 = lean_ctor_get(x_13, 0);
-x_18 = lean_ctor_get(x_13, 1);
-lean_inc(x_18);
-lean_inc(x_17);
-lean_dec(x_13);
-x_19 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_19, 0, x_9);
-lean_ctor_set(x_19, 1, x_17);
-x_20 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_20, 0, x_19);
-lean_ctor_set(x_20, 1, x_18);
-return x_20;
-}
-}
-}
-lean_object* l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg___boxed), 4, 0);
-return x_2;
-}
-}
 lean_object* l_Lean_Elab_elabAttr___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__4___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
 _start:
 {
@@ -894,7 +822,7 @@ x_14 = l_Lean_Elab_elabAttr___rarg___lambda__3___closed__3;
 x_15 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_15, 0, x_13);
 lean_ctor_set(x_15, 1, x_14);
-x_16 = l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_15, x_3, x_4, x_8);
+x_16 = l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(x_15, x_3, x_4, x_8);
 x_17 = !lean_is_exclusive(x_16);
 if (x_17 == 0)
 {
@@ -951,7 +879,7 @@ x_13 = lean_ctor_get(x_2, 6);
 lean_dec(x_13);
 lean_ctor_set(x_2, 6, x_11);
 x_14 = l_Lean_Elab_elabAttr___rarg___closed__3;
-x_15 = l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_14, x_2, x_3, x_10);
+x_15 = l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(x_14, x_2, x_3, x_10);
 x_16 = !lean_is_exclusive(x_15);
 if (x_16 == 0)
 {
@@ -996,7 +924,7 @@ lean_ctor_set(x_26, 4, x_24);
 lean_ctor_set(x_26, 5, x_25);
 lean_ctor_set(x_26, 6, x_11);
 x_27 = l_Lean_Elab_elabAttr___rarg___closed__3;
-x_28 = l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_27, x_26, x_3, x_10);
+x_28 = l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(x_27, x_26, x_3, x_10);
 x_29 = lean_ctor_get(x_28, 0);
 lean_inc(x_29);
 x_30 = lean_ctor_get(x_28, 1);
@@ -1033,7 +961,7 @@ return x_36;
 }
 }
 }
-lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__6(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
 _start:
 {
 uint8_t x_8; 
@@ -1107,7 +1035,7 @@ x_7 = lean_usize_of_nat(x_6);
 lean_dec(x_6);
 x_8 = 0;
 x_9 = l_Array_empty___closed__1;
-x_10 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__6(x_5, x_7, x_8, x_9, x_2, x_3, x_4);
+x_10 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5(x_5, x_7, x_8, x_9, x_2, x_3, x_4);
 lean_dec(x_5);
 if (lean_obj_tag(x_10) == 0)
 {
@@ -1166,7 +1094,7 @@ lean_dec(x_6);
 return x_7;
 }
 }
-lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__7___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__6___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
 lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; 
@@ -1185,7 +1113,7 @@ lean_object* x_11; lean_object* x_12;
 x_11 = lean_ctor_get(x_3, 6);
 lean_dec(x_11);
 lean_ctor_set(x_3, 6, x_9);
-x_12 = l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_2, x_3, x_4, x_8);
+x_12 = l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(x_2, x_3, x_4, x_8);
 return x_12;
 }
 else
@@ -1212,16 +1140,16 @@ lean_ctor_set(x_19, 3, x_16);
 lean_ctor_set(x_19, 4, x_17);
 lean_ctor_set(x_19, 5, x_18);
 lean_ctor_set(x_19, 6, x_9);
-x_20 = l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_2, x_19, x_4, x_8);
+x_20 = l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(x_2, x_19, x_4, x_8);
 return x_20;
 }
 }
 }
-lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__7(lean_object* x_1) {
+lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__6(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_Lean_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__7___rarg___boxed), 5, 0);
+x_2 = lean_alloc_closure((void*)(l_Lean_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__6___rarg___boxed), 5, 0);
 return x_2;
 }
 }
@@ -1480,7 +1408,7 @@ if (x_18 == 0)
 lean_object* x_19; lean_object* x_20; uint8_t x_21; 
 lean_dec(x_6);
 x_19 = l_Lean_Elab_elabModifiers___rarg___lambda__3___closed__7;
-x_20 = l_Lean_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__7___rarg(x_13, x_19, x_7, x_8, x_9);
+x_20 = l_Lean_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__6___rarg(x_13, x_19, x_7, x_8, x_9);
 lean_dec(x_13);
 x_21 = !lean_is_exclusive(x_20);
 if (x_21 == 0)
@@ -1602,7 +1530,7 @@ x_31 = l_Lean_Meta_forallTelescopeCompatibleAux___rarg___lambda__4___closed__5;
 x_32 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_32, 0, x_30);
 lean_ctor_set(x_32, 1, x_31);
-x_33 = l_Lean_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__7___rarg(x_21, x_32, x_2, x_3, x_4);
+x_33 = l_Lean_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__6___rarg(x_21, x_32, x_2, x_3, x_4);
 lean_dec(x_21);
 x_34 = !lean_is_exclusive(x_33);
 if (x_34 == 0)
@@ -1672,7 +1600,7 @@ x_49 = l_Lean_Meta_forallTelescopeCompatibleAux___rarg___lambda__4___closed__5;
 x_50 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_50, 0, x_48);
 lean_ctor_set(x_50, 1, x_49);
-x_51 = l_Lean_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__7___rarg(x_38, x_50, x_2, x_3, x_4);
+x_51 = l_Lean_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__6___rarg(x_38, x_50, x_2, x_3, x_4);
 lean_dec(x_38);
 x_52 = lean_ctor_get(x_51, 0);
 lean_inc(x_52);
@@ -1699,7 +1627,7 @@ return x_55;
 }
 }
 }
-lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9___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* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
 _start:
 {
 lean_object* x_7; 
@@ -1746,13 +1674,13 @@ x_17 = l_Lean_Elab_throwAlreadyDeclaredUniverseLevel___rarg___closed__4;
 x_18 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_18, 0, x_16);
 lean_ctor_set(x_18, 1, x_17);
-x_19 = l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_18, x_4, x_5, x_6);
+x_19 = l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(x_18, x_4, x_5, x_6);
 return x_19;
 }
 }
 }
 }
-lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9___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* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8___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) {
 _start:
 {
 lean_object* x_7; uint8_t x_8; 
@@ -1766,7 +1694,7 @@ if (x_8 == 0)
 {
 lean_object* x_9; lean_object* x_10; 
 x_9 = lean_box(0);
-x_10 = l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9___lambda__1(x_1, x_2, x_9, x_4, x_5, x_6);
+x_10 = l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8___lambda__1(x_1, x_2, x_9, x_4, x_5, x_6);
 return x_10;
 }
 else
@@ -1783,7 +1711,7 @@ x_14 = l_Lean_Elab_throwAlreadyDeclaredUniverseLevel___rarg___closed__4;
 x_15 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_15, 0, x_13);
 lean_ctor_set(x_15, 1, x_14);
-x_16 = l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_15, x_4, x_5, x_6);
+x_16 = l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(x_15, x_4, x_5, x_6);
 x_17 = !lean_is_exclusive(x_16);
 if (x_17 == 0)
 {
@@ -1805,7 +1733,7 @@ return x_20;
 }
 }
 }
-lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8(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; uint8_t x_9; 
@@ -1824,7 +1752,7 @@ if (x_9 == 0)
 {
 lean_object* x_10; lean_object* x_11; 
 x_10 = lean_box(0);
-x_11 = l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9___lambda__2(x_1, x_8, x_10, x_2, x_3, x_7);
+x_11 = l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8___lambda__2(x_1, x_8, x_10, x_2, x_3, x_7);
 return x_11;
 }
 else
@@ -1846,7 +1774,7 @@ x_16 = l_Lean_Elab_throwAlreadyDeclaredUniverseLevel___rarg___closed__4;
 x_17 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_17, 0, x_15);
 lean_ctor_set(x_17, 1, x_16);
-x_18 = l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_17, x_2, x_3, x_7);
+x_18 = l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(x_17, x_2, x_3, x_7);
 x_19 = !lean_is_exclusive(x_18);
 if (x_19 == 0)
 {
@@ -1883,7 +1811,7 @@ x_27 = l_Lean_Elab_throwAlreadyDeclaredUniverseLevel___rarg___closed__4;
 x_28 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_28, 0, x_26);
 lean_ctor_set(x_28, 1, x_27);
-x_29 = l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_28, x_2, x_3, x_7);
+x_29 = l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(x_28, x_2, x_3, x_7);
 x_30 = !lean_is_exclusive(x_29);
 if (x_30 == 0)
 {
@@ -1906,7 +1834,7 @@ return x_33;
 }
 }
 }
-lean_object* l_Lean_setEnv___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__10(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+lean_object* l_Lean_setEnv___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9(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; uint8_t x_8; 
@@ -1994,7 +1922,7 @@ return x_28;
 }
 }
 }
-lean_object* l_Lean_Elab_applyVisibility___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+lean_object* l_Lean_Elab_applyVisibility___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__7(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
 switch (x_1) {
@@ -2002,7 +1930,7 @@ case 0:
 {
 lean_object* x_6; 
 lean_inc(x_2);
-x_6 = l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9(x_2, x_3, x_4, x_5);
+x_6 = l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8(x_2, x_3, x_4, x_5);
 if (lean_obj_tag(x_6) == 0)
 {
 uint8_t x_7; 
@@ -2056,7 +1984,7 @@ case 1:
 lean_object* x_15; 
 lean_inc(x_3);
 lean_inc(x_2);
-x_15 = l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9(x_2, x_3, x_4, x_5);
+x_15 = l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8(x_2, x_3, x_4, x_5);
 if (lean_obj_tag(x_15) == 0)
 {
 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; uint8_t x_24; 
@@ -2075,7 +2003,7 @@ lean_dec(x_18);
 x_21 = l_Lean_protectedExt;
 lean_inc(x_2);
 x_22 = l_Lean_PersistentEnvExtension_addEntry___rarg(x_21, x_20, x_2);
-x_23 = l_Lean_setEnv___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__10(x_22, x_3, x_4, x_19);
+x_23 = l_Lean_setEnv___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9(x_22, x_3, x_4, x_19);
 lean_dec(x_3);
 x_24 = !lean_is_exclusive(x_23);
 if (x_24 == 0)
@@ -2137,7 +2065,7 @@ lean_inc(x_35);
 lean_dec(x_33);
 x_36 = l_Lean_mkPrivateName(x_35, x_2);
 lean_inc(x_36);
-x_37 = l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9(x_36, x_3, x_4, x_34);
+x_37 = l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8(x_36, x_3, x_4, x_34);
 if (lean_obj_tag(x_37) == 0)
 {
 uint8_t x_38; 
@@ -2204,7 +2132,7 @@ lean_dec(x_12);
 lean_inc(x_13);
 x_14 = l_Lean_Name_append___main(x_2, x_13);
 x_15 = lean_ctor_get_uint8(x_3, sizeof(void*)*2);
-x_16 = l_Lean_Elab_applyVisibility___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8(x_15, x_14, x_5, x_6, x_7);
+x_16 = l_Lean_Elab_applyVisibility___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__7(x_15, x_14, x_5, x_6, x_7);
 if (x_10 == 0)
 {
 if (lean_obj_tag(x_16) == 0)
@@ -2398,7 +2326,7 @@ lean_object* x_15; lean_object* x_16; uint8_t x_17;
 lean_dec(x_3);
 lean_dec(x_1);
 x_15 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___lambda__2___closed__3;
-x_16 = l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_15, x_6, x_7, x_8);
+x_16 = l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(x_15, x_6, x_7, x_8);
 x_17 = !lean_is_exclusive(x_16);
 if (x_17 == 0)
 {
@@ -2523,7 +2451,7 @@ lean_object* x_30; lean_object* x_31; uint8_t x_32;
 lean_dec(x_20);
 lean_dec(x_11);
 x_30 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___closed__3;
-x_31 = l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_30, x_4, x_5, x_23);
+x_31 = l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(x_30, x_4, x_5, x_23);
 x_32 = !lean_is_exclusive(x_31);
 if (x_32 == 0)
 {
@@ -2664,7 +2592,7 @@ lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean
 lean_dec(x_52);
 lean_dec(x_11);
 x_62 = l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___closed__3;
-x_63 = l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_62, x_50, x_5, x_55);
+x_63 = l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(x_62, x_50, x_5, x_55);
 x_64 = lean_ctor_get(x_63, 0);
 lean_inc(x_64);
 x_65 = lean_ctor_get(x_63, 1);
@@ -2766,15 +2694,6 @@ return x_81;
 }
 }
 }
-lean_object* l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg___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_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_1, x_2, x_3, x_4);
-lean_dec(x_3);
-return x_5;
-}
-}
 lean_object* l_Lean_Elab_elabAttr___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__4___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) {
 _start:
 {
@@ -2818,7 +2737,7 @@ lean_dec(x_1);
 return x_5;
 }
 }
-lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__6___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* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___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) {
 _start:
 {
 size_t x_8; size_t x_9; lean_object* x_10; 
@@ -2826,7 +2745,7 @@ x_8 = lean_unbox_usize(x_2);
 lean_dec(x_2);
 x_9 = lean_unbox_usize(x_3);
 lean_dec(x_3);
-x_10 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__6(x_1, x_8, x_9, x_4, x_5, x_6, x_7);
+x_10 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5(x_1, x_8, x_9, x_4, x_5, x_6, x_7);
 lean_dec(x_6);
 lean_dec(x_1);
 return x_10;
@@ -2852,11 +2771,11 @@ lean_dec(x_1);
 return x_5;
 }
 }
-lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__7___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__6___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
 lean_object* x_6; 
-x_6 = l_Lean_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__7___rarg(x_1, x_2, x_3, x_4, x_5);
+x_6 = l_Lean_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__6___rarg(x_1, x_2, x_3, x_4, x_5);
 lean_dec(x_4);
 lean_dec(x_1);
 return x_6;
@@ -2916,52 +2835,52 @@ lean_dec(x_1);
 return x_5;
 }
 }
-lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9___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* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8___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) {
 _start:
 {
 lean_object* x_7; 
-x_7 = l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6);
+x_7 = l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6);
 lean_dec(x_5);
 lean_dec(x_3);
 return x_7;
 }
 }
-lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9___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* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8___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) {
 _start:
 {
 lean_object* x_7; 
-x_7 = l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9___lambda__2(x_1, x_2, x_3, x_4, x_5, x_6);
+x_7 = l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8___lambda__2(x_1, x_2, x_3, x_4, x_5, x_6);
 lean_dec(x_5);
 lean_dec(x_3);
 return x_7;
 }
 }
-lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8___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_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9(x_1, x_2, x_3, x_4);
+x_5 = l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8(x_1, x_2, x_3, x_4);
 lean_dec(x_3);
 return x_5;
 }
 }
-lean_object* l_Lean_setEnv___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__10___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+lean_object* l_Lean_setEnv___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9___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_setEnv___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__10(x_1, x_2, x_3, x_4);
+x_5 = l_Lean_setEnv___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__9(x_1, x_2, x_3, x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 return x_5;
 }
 }
-lean_object* l_Lean_Elab_applyVisibility___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+lean_object* l_Lean_Elab_applyVisibility___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__7___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {
 uint8_t x_6; lean_object* x_7; 
 x_6 = lean_unbox(x_1);
 lean_dec(x_1);
-x_7 = l_Lean_Elab_applyVisibility___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8(x_6, x_2, x_3, x_4, x_5);
+x_7 = l_Lean_Elab_applyVisibility___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__7(x_6, x_2, x_3, x_4, x_5);
 lean_dec(x_4);
 return x_7;
 }
@@ -3047,7 +2966,7 @@ else
 {
 lean_object* x_9; lean_object* x_10; 
 x_9 = l_Lean_Elab_Command_checkValidFieldModifier___lambda__1___closed__3;
-x_10 = l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_9, x_3, x_4, x_5);
+x_10 = l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(x_9, x_3, x_4, x_5);
 return x_10;
 }
 }
@@ -3093,7 +3012,7 @@ if (x_9 == 0)
 {
 lean_object* x_10; lean_object* x_11; uint8_t x_12; 
 x_10 = l_Lean_Elab_Command_checkValidFieldModifier___lambda__2___closed__3;
-x_11 = l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_10, x_3, x_4, x_5);
+x_11 = l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(x_10, x_3, x_4, x_5);
 x_12 = !lean_is_exclusive(x_11);
 if (x_12 == 0)
 {
@@ -3166,7 +3085,7 @@ else
 {
 lean_object* x_9; lean_object* x_10; uint8_t x_11; 
 x_9 = l_Lean_Elab_Command_checkValidFieldModifier___lambda__3___closed__3;
-x_10 = l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_9, x_3, x_4, x_5);
+x_10 = l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(x_9, x_3, x_4, x_5);
 x_11 = !lean_is_exclusive(x_10);
 if (x_11 == 0)
 {
@@ -3232,7 +3151,7 @@ else
 {
 lean_object* x_9; lean_object* x_10; uint8_t x_11; 
 x_9 = l_Lean_Elab_Command_checkValidFieldModifier___lambda__4___closed__3;
-x_10 = l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_9, x_3, x_4, x_5);
+x_10 = l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(x_9, x_3, x_4, x_5);
 x_11 = !lean_is_exclusive(x_10);
 if (x_11 == 0)
 {
@@ -3298,7 +3217,7 @@ else
 {
 lean_object* x_8; lean_object* x_9; uint8_t x_10; 
 x_8 = l_Lean_Elab_Command_checkValidFieldModifier___closed__3;
-x_9 = l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_8, x_2, x_3, x_4);
+x_9 = l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(x_8, x_2, x_3, x_4);
 x_10 = !lean_is_exclusive(x_9);
 if (x_10 == 0)
 {
@@ -3423,7 +3342,7 @@ lean_object* x_15; uint8_t x_16; lean_object* x_17;
 lean_inc(x_2);
 x_15 = l_Lean_Name_append___main(x_1, x_2);
 x_16 = lean_ctor_get_uint8(x_3, sizeof(void*)*2);
-x_17 = l_Lean_Elab_applyVisibility___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8(x_16, x_15, x_12, x_13, x_14);
+x_17 = l_Lean_Elab_applyVisibility___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__7(x_16, x_15, x_12, x_13, x_14);
 if (lean_obj_tag(x_17) == 0)
 {
 uint8_t x_18; 
@@ -3655,7 +3574,7 @@ x_46 = l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Ela
 x_47 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_47, 0, x_45);
 lean_ctor_set(x_47, 1, x_46);
-x_48 = l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_47, x_33, x_13, x_25);
+x_48 = l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(x_47, x_33, x_13, x_25);
 x_49 = !lean_is_exclusive(x_48);
 if (x_49 == 0)
 {
@@ -3866,7 +3785,7 @@ lean_object* x_17; lean_object* x_18; uint8_t x_19;
 lean_dec(x_5);
 lean_dec(x_4);
 x_17 = l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__2___lambda__2___closed__3;
-x_18 = l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_17, x_8, x_9, x_10);
+x_18 = l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(x_17, x_8, x_9, x_10);
 x_19 = !lean_is_exclusive(x_18);
 if (x_19 == 0)
 {
@@ -3967,7 +3886,7 @@ lean_object* x_22; lean_object* x_23; uint8_t x_24;
 lean_dec(x_12);
 lean_dec(x_3);
 x_22 = l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__2___lambda__3___closed__3;
-x_23 = l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_22, x_6, x_7, x_15);
+x_23 = l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(x_22, x_6, x_7, x_15);
 x_24 = !lean_is_exclusive(x_23);
 if (x_24 == 0)
 {
@@ -4196,7 +4115,7 @@ lean_dec(x_15);
 lean_dec(x_13);
 lean_dec(x_6);
 x_34 = l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__2___closed__9;
-x_35 = l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__5___rarg(x_34, x_29, x_8, x_21);
+x_35 = l_Lean_throwError___at_Lean_Elab_Command_checkValidInductiveModifier___spec__1___rarg(x_34, x_29, x_8, x_21);
 x_36 = !lean_is_exclusive(x_35);
 if (x_36 == 0)
 {
@@ -8825,7 +8744,7 @@ lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_removeUnused(l
 _start:
 {
 lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
-x_11 = l___private_Lean_Elab_Inductive_26__removeUnused___closed__1;
+x_11 = l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_removeUnused___closed__1;
 x_12 = lean_st_mk_ref(x_11, x_10);
 x_13 = lean_ctor_get(x_12, 0);
 lean_inc(x_13);
@@ -9787,57 +9706,7 @@ x_2 = lean_alloc_closure((void*)(l___private_Lean_Elab_Structure_0__Lean_Elab_Co
 return x_2;
 }
 }
-lean_object* l_Lean_Meta_getLevel___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
-_start:
-{
-lean_object* x_9; 
-x_9 = l___private_Lean_Meta_InferType_4__getLevelImp(x_1, x_4, x_5, x_6, x_7, x_8);
-return x_9;
-}
-}
-lean_object* l_Lean_Meta_instantiateLevelMVars___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___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, lean_object* x_7, lean_object* x_8) {
-_start:
-{
-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; uint8_t x_17; 
-x_9 = lean_st_ref_get(x_5, x_8);
-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, 0);
-lean_inc(x_12);
-lean_dec(x_10);
-x_13 = l_Lean_MetavarContext_instantiateLevelMVars___main(x_1, x_12);
-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 = l_Lean_Meta_setMCtx___at___private_Lean_Meta_Basic_6__liftMkBindingM___spec__1(x_15, x_4, x_5, x_6, x_7, x_11);
-x_17 = !lean_is_exclusive(x_16);
-if (x_17 == 0)
-{
-lean_object* x_18; 
-x_18 = lean_ctor_get(x_16, 0);
-lean_dec(x_18);
-lean_ctor_set(x_16, 0, x_14);
-return x_16;
-}
-else
-{
-lean_object* x_19; lean_object* x_20; 
-x_19 = lean_ctor_get(x_16, 1);
-lean_inc(x_19);
-lean_dec(x_16);
-x_20 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_20, 0, x_14);
-lean_ctor_set(x_20, 1, x_19);
-return x_20;
-}
-}
-}
-lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__3(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, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
+lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
 _start:
 {
 lean_object* x_14; uint8_t x_15; 
@@ -9895,14 +9764,14 @@ lean_inc(x_25);
 x_26 = lean_ctor_get(x_24, 1);
 lean_inc(x_26);
 lean_dec(x_24);
-x_27 = l_Lean_Meta_instantiateLevelMVars___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__2(x_25, x_7, x_8, x_9, x_10, x_11, x_12, x_26);
+x_27 = l_Lean_Meta_instantiateLevelMVars___at_Lean_Elab_Command_shouldInferResultUniverse___spec__1(x_25, x_7, x_8, x_9, x_10, x_11, x_12, x_26);
 x_28 = lean_ctor_get(x_27, 0);
 lean_inc(x_28);
 x_29 = lean_ctor_get(x_27, 1);
 lean_inc(x_29);
 lean_dec(x_27);
 lean_inc(x_2);
-x_30 = l_Lean_Elab_Command_accLevelAtCtor___main(x_28, x_1, x_2, x_6);
+x_30 = l_Lean_Elab_Command_accLevelAtCtor(x_28, x_1, x_2, x_6);
 if (lean_obj_tag(x_30) == 0)
 {
 lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; uint8_t x_35; 
@@ -10021,39 +9890,15 @@ _start:
 lean_object* x_11; lean_object* x_12; lean_object* x_13; 
 x_11 = lean_unsigned_to_nat(0u);
 x_12 = l_Array_empty___closed__1;
-x_13 = l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__3(x_1, x_2, x_3, x_3, x_11, x_12, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
+x_13 = l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__1(x_1, x_2, x_3, x_3, x_11, x_12, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
 return x_13;
 }
 }
-lean_object* l_Lean_Meta_getLevel___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__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_Meta_getLevel___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__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_Meta_instantiateLevelMVars___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__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_instantiateLevelMVars___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__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);
-lean_dec(x_2);
-return x_9;
-}
-}
-lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__3___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, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
+lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__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, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
 _start:
 {
 lean_object* x_14; 
-x_14 = l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__3(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
+x_14 = l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_collectUniversesFromFields___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
 lean_dec(x_8);
 lean_dec(x_4);
 lean_dec(x_3);
@@ -10643,7 +10488,7 @@ _start:
 {
 lean_object* x_11; lean_object* x_12; lean_object* x_13; 
 x_11 = lean_unsigned_to_nat(0u);
-x_12 = l___private_Lean_Elab_Inductive_29__collectLevelParamsInInductive___closed__1;
+x_12 = l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_collectLevelParamsInInductive___closed__1;
 lean_inc(x_9);
 lean_inc(x_8);
 lean_inc(x_7);
@@ -11681,7 +11526,7 @@ lean_dec(x_9);
 x_12 = lean_ctor_get(x_10, 0);
 lean_inc(x_12);
 lean_dec(x_10);
-x_13 = l___private_Lean_Elab_Inductive_34__mkAuxConstructions___closed__2;
+x_13 = l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkAuxConstructions___closed__2;
 lean_inc(x_12);
 x_14 = l_Lean_Environment_contains(x_12, x_13);
 x_15 = l_Lean_Expr_eq_x3f___closed__2;