chore: update stage0

stage0/src/Init/Lean/Elab/Command.lean

@@ -41,6 +41,7 @@ structure Context :=
 (fileMap        : FileMap)
 (stateRef       : IO.Ref State)
 (cmdPos         : String.Pos := 0)
+(macroStack     : List Syntax := [])
 (currMacroScope : MacroScope := 0)
 
 abbrev CommandElabCoreM (ε) := ReaderT Context (EIO ε)
@@ -79,6 +80,46 @@ instance CommandElabM.monadLog : MonadLog CommandElabM :=
   getFileName := do ctx ← read; pure ctx.fileName,
   logMessage  := fun msg => modify $ fun s => { messages := s.messages.add msg, .. s } }
 
+/- If `ref` does not have position information, then try to use macroStack -/
+private def getBetterRef (ref : Syntax) : CommandElabM Syntax :=
+match ref.getPos with
+| some _ => pure ref
+| none   => do
+  ctx ← read;
+  match ctx.macroStack.find? $ fun (macro : Syntax) => macro.getPos != none with
+  | some macro => pure macro
+  | none       => pure ref
+
+private def prettyPrint (stx : Syntax) : CommandElabM Format :=
+match stx.reprint with -- TODO use syntax pretty printer
+| some str => pure $ format str
+| none     => pure $ format stx
+
+private def addMacroStack (msgData : MessageData) : CommandElabM MessageData := do
+ctx ← read;
+if ctx.macroStack.isEmpty then pure msgData
+else
+  ctx.macroStack.foldlM
+    (fun (msgData : MessageData) (macro : Syntax) => do
+      macroFmt ← prettyPrint macro;
+      pure (msgData ++ Format.line ++ "while expanding" ++ MessageData.nest 2 (Format.line ++ macroFmt)))
+    msgData
+
+/--
+  Throws an error with the given `msgData` and extracting position information from `ref`.
+  If `ref` does not contain position information, then use `cmdPos` -/
+def throwError {α} (ref : Syntax) (msgData : MessageData) : CommandElabM α := do
+ref ← getBetterRef ref;
+msgData ← addMacroStack msgData;
+msg ← mkMessage msgData MessageSeverity.error ref;
+throw msg
+
+def throwUnexpectedSyntax {α} (ref : Syntax) (expectedMsg : Option String := none) : CommandElabM α := do
+refFmt ← prettyPrint ref;
+match expectedMsg with
+| none    => throwError ref ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
+| some ex => throwError ref ("unexpected syntax, expected '" ++ ex ++ "'" ++ MessageData.nest 2 (Format.line ++ refFmt))
+
 protected def getCurrMacroScope : CommandElabM Nat := do
 ctx ← read;
 pure ctx.currMacroScope
@@ -145,9 +186,13 @@ stx.ifNode
     | none      => throwError stx ("command '" ++ toString k ++ "' has not been implemented"))
   (fun _ => throwError stx ("unexpected command"))
 
+/- Elaborate `x` with `stx` on the macro stack -/
+@[inline] def withMacroExpansion {α} (stx : Syntax) (x : CommandElabM α) : CommandElabM α :=
+adaptReader (fun (ctx : Context) => { macroStack := stx :: ctx.macroStack, .. ctx }) x
+
 /-- Adapt a syntax transformation to a regular, command-producing elaborator. -/
 def adaptExpander (exp : Syntax → CommandElabM Syntax) : CommandElab :=
-fun stx => do
+fun stx => withMacroExpansion stx.val $ do
   stx ← exp stx.val;
   elabCommand stx
 
@@ -157,6 +202,7 @@ let scope := s.scopes.head!;
   fileName       := ctx.fileName,
   fileMap        := ctx.fileMap,
   cmdPos         := ctx.cmdPos,
+  macroStack     := ctx.macroStack,
   currMacroScope := ctx.currMacroScope,
   currNamespace  := scope.currNamespace,
   levelNames     := scope.levelNames,
@@ -229,14 +275,15 @@ private def addNamespace (ref : Syntax) (header : Name) : CommandElabM Unit :=
 addScopes ref "namespace" true header
 
 @[builtinCommandElab «namespace»] def elabNamespace : CommandElab :=
-fun stx => addNamespace stx.val (stx.getIdAt 1)
+fun stx => match_syntax stx.val with
+  | `(namespace $n) => addNamespace stx.val n.getId
+  | _               => throwUnexpectedSyntax stx.val "namespace"
 
 @[builtinCommandElab «section»] def elabSection : CommandElab :=
-fun stx => do
-  let header? := (stx.getArg 1).getOptionalIdent?;
-  match header? with
-  | some header => addScopes stx.val "section" false header
-  | none        => do currNamespace ← getCurrNamespace; addScope "section" "" currNamespace
+fun stx => match_syntax stx.val with
+  | `(section $header:ident) => addScopes stx.val "section" false header.getId
+  | `(section)               => do currNamespace ← getCurrNamespace; addScope "section" "" currNamespace
+  | _                        => throwUnexpectedSyntax stx.val "section"
 
 def getScopes : CommandElabM (List Scope) := do
 s ← get; pure s.scopes

stage0/src/Init/Lean/Elab/Declaration.lean

@@ -101,7 +101,7 @@ withDeclId declId $ fun name => do
     type ← Term.mkForall typeStx xs type;
     (type, _) ← Term.mkForallUsedOnly typeStx vars type;
     type ← Term.levelMVarToParam type;
-    let usedParams  := collectLevelParams type;
+    let usedParams  := (collectLevelParams {} type).params;
     let levelParams := sortDeclLevelParams explictLevelNames usedParams;
     pure $ Declaration.axiomDecl {
       name     := declName,

stage0/src/Init/Lean/Elab/Definition.lean

@@ -4,16 +4,31 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
+import Init.Lean.Util.CollectLevelParams
+import Init.Lean.Util.CollectFVars
 import Init.Lean.Elab.DeclModifiers
+import Init.Lean.Elab.TermBinders
 
 namespace Lean
 namespace Elab
-
 namespace Command
 
 inductive DefKind
 | «def» | «theorem» | «example» | «opaque»
 
+def DefKind.isTheorem : DefKind → Bool
+| DefKind.theorem => true
+| _               => false
+
+def DefKind.isDefOrOpaque : DefKind → Bool
+| DefKind.def    => true
+| DefKind.opaque => true
+| _              => false
+
+def DefKind.isExample : DefKind → Bool
+| DefKind.example => true
+| _               => false
+
 structure DefView :=
 (kind          : DefKind)
 (ref           : Syntax)
@@ -23,24 +38,116 @@ structure DefView :=
 (type?         : Option Syntax)
 (val           : Syntax)
 
+def collectUsedFVars (ref : Syntax) (used : CollectFVars.State) (e : Expr) : TermElabM CollectFVars.State := do
+e ← Term.instantiateMVars ref e;
+pure $ collectFVars used e
+
+def collectUsedFVarsAtFVars (ref : Syntax) (used : CollectFVars.State) (fvars : Array Expr) : TermElabM CollectFVars.State :=
+fvars.foldlM
+  (fun used fvar => do
+    fvarType ← Term.inferType ref fvar;
+    collectUsedFVars ref used fvarType)
+  used
+
+def removeUnused (ref : Syntax) (vars : Array Expr) (xs : Array Expr) (e : Expr) (eType : Expr)
+    : TermElabM (LocalContext × LocalInstances × Array Expr) := do
+let used : CollectFVars.State := {};
+used ← collectUsedFVars ref used eType;
+used ← collectUsedFVars ref used e;
+used ← collectUsedFVarsAtFVars ref used xs;
+localInsts ← Term.getLocalInsts;
+lctx ← Term.getLCtx;
+(lctx, localInsts, newVars, _) ← vars.foldrM
+  (fun var (result : LocalContext × LocalInstances × Array Expr × CollectFVars.State) =>
+    let (lctx, localInsts, newVars, used) := result;
+    if used.fvarSet.contains var.fvarId! then do
+      varType ← Term.inferType ref var;
+      used ← collectUsedFVars ref used varType;
+      pure (lctx, localInsts, newVars.push var, used)
+    else
+      pure (lctx.erase var.fvarId!, localInsts.erase var.fvarId!, newVars, used))
+  (lctx, localInsts, #[], used);
+pure (lctx, localInsts, newVars.reverse)
+
+def withUsedWhen {α} (ref : Syntax) (vars : Array Expr) (xs : Array Expr) (e : Expr) (eType : Expr) (cond : Bool) (k : Array Expr → TermElabM α) : TermElabM α :=
+if cond then do
+ (lctx, localInsts, vars) ← removeUnused ref vars xs e eType;
+ Term.withLCtx lctx localInsts $ k vars
+else
+ k vars
+
+def withUsedWhen' {α} (ref : Syntax) (vars : Array Expr) (xs : Array Expr) (e : Expr) (cond : Bool) (k : Array Expr → TermElabM α) : TermElabM α :=
+let dummyExpr := mkSort levelOne;
+withUsedWhen ref vars xs e dummyExpr cond k
+
+def mkDef (view : DefView) (declName : Name) (explictLevelNames : List Name) (vars : Array Expr) (xs : Array Expr) (type : Expr) (val : Expr)
+    : TermElabM (Option Declaration) := do
+let ref := view.ref;
+Term.synthesizeSyntheticMVars false;
+type    ← Term.instantiateMVars ref type;
+val     ← Term.instantiateMVars view.val val;
+valType ← Term.inferType view.val val;
+val     ← Term.ensureHasType ref type valType val;
+if view.kind.isExample then pure none
+else withUsedWhen ref vars xs val type view.kind.isDefOrOpaque $ fun vars => do
+  type ← Term.mkForall ref xs type;
+  type ← Term.mkForall ref vars type;
+  val  ← Term.mkLambda ref xs val;
+  val  ← Term.mkLambda ref vars val;
+  let usedParams : CollectLevelParams.State := {};
+  let usedParams  := collectLevelParams usedParams type;
+  let usedParams  := collectLevelParams usedParams val;
+  let levelParams := sortDeclLevelParams explictLevelNames usedParams.params;
+  match view.kind with
+  | DefKind.theorem =>
+    -- TODO theorem elaboration in parallel
+    pure $ some $ Declaration.thmDecl { name := declName, lparams := levelParams, type := type, value := Task.pure val }
+  | DefKind.opaque  =>
+    pure $ some $ Declaration.opaqueDecl { name := declName, lparams := levelParams, type := type, value := val, isUnsafe := view.modifiers.isUnsafe }
+  | DefKind.def =>
+    pure $ some $ Declaration.defnDecl {
+      name := declName, lparams := levelParams, type := type, value := val,
+      hints := ReducibilityHints.regular 0, -- TODO
+      isUnsafe := view.modifiers.isUnsafe }
+  | _ => unreachable!
+
+def elabDefVal (defVal : Syntax) (expectedType : Expr) : TermElabM Expr := do
+let kind := defVal.getKind;
+if kind == `Lean.Parser.Command.declValSimple then
+  -- parser! " := " >> termParser
+  Term.elabTerm (defVal.getArg 1) expectedType
+else if kind == `Lean.Parser.Command.declValEqns then
+  Term.throwError defVal "equations have not been implemented yet"
+else
+  Term.throwUnexpectedSyntax defVal "definition body"
+
 def elabDefLike (view : DefView) : CommandElabM Unit :=
+let ref := view.ref;
 withDeclId view.declId $ fun name => do
-  currNamespace ← getCurrNamespace;
-  runTermElabM $ fun vars => Term.elabBinders view.binders.getArgs $ fun xs =>
+  declName          ← mkDeclName view.modifiers name;
+  applyAttributes ref declName view.modifiers.attrs AttributeApplicationTime.beforeElaboration;
+  explictLevelNames ← getLevelNames;
+  decl? ← runTermElabM $ fun vars => Term.elabBinders view.binders.getArgs $ fun xs =>
     match view.type? with
     | some typeStx => do
-      type    ← Term.elabType typeStx;
+      type ← Term.elabType typeStx;
       Term.synthesizeSyntheticMVars false;
-      type    ← Term.instantiateMVars typeStx type;
-      defType ← Term.mkForall typeStx xs type;
-      -- TODO: unassigned universe metavariables to new parameters
-      -- TODO: if theorem, filter unused vars
-      Term.dbgTrace (">>> " ++ toString type);
-      pure ()
-    | none => do
+      type ← Term.instantiateMVars typeStx type;
+      withUsedWhen' ref vars xs type view.kind.isTheorem $ fun vars => do
+        val  ← elabDefVal view.val type;
+        mkDef view declName explictLevelNames vars xs type val
+    | none => do {
       type ← Term.mkFreshTypeMVar view.binders;
-
-      pure ()
+      val  ← elabDefVal view.val type;
+      mkDef view declName explictLevelNames vars xs type val
+    };
+  match decl? with
+  | none      => pure ()
+  | some decl => do
+    addDecl ref decl;
+    applyAttributes ref declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking;
+    -- TODO invoke compiler
+    applyAttributes ref declName view.modifiers.attrs AttributeApplicationTime.afterCompilation
 
 end Command
 end Elab

stage0/src/Init/Lean/MetavarContext.lean

@@ -234,6 +234,12 @@ i₁.fvar == i₂.fvar
 
 instance LocalInstance.hasBeq : HasBeq LocalInstance := ⟨LocalInstance.beq⟩
 
+/-- Remove local instance with the given `fvarId`. Do nothing if `localInsts` does not contain any free variable with id `fvarId`. -/
+def LocalInstances.erase (localInsts : LocalInstances) (fvarId : FVarId) : LocalInstances :=
+match localInsts.findIdx? (fun inst => inst.fvar.fvarId! == fvarId) with
+| some idx => localInsts.eraseIdx idx
+| _        => localInsts
+
 inductive MetavarKind
 | natural
 | synthetic

stage0/src/Init/Lean/Util/CollectFVars.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Expr
+
+namespace Lean
+
+namespace CollectFVars
+
+structure State :=
+(visitedExpr  : ExprSet  := {})
+(fvarSet      : NameSet  := {})
+
+instance State.inhabited : Inhabited State := ⟨{}⟩
+
+abbrev Visitor := State → State
+
+@[inline] def visit (f : Expr → Visitor) (e : Expr) : Visitor :=
+fun s =>
+  if !e.hasFVar || s.visitedExpr.contains e then s
+  else f e { visitedExpr := s.visitedExpr.insert e, .. s }
+
+partial def main : Expr → Visitor
+| Expr.proj _ _ e _    => visit main e
+| Expr.forallE _ d b _ => visit main b ∘ visit main d
+| Expr.lam _ d b _     => visit main b ∘ visit main d
+| Expr.letE _ t v b _  => visit main b ∘ visit main v ∘ visit main t
+| Expr.app f a _       => visit main a ∘ visit main f
+| Expr.mdata _ b _     => visit main b
+| Expr.fvar fvarId _   => fun s => { fvarSet := s.fvarSet.insert fvarId, .. s }
+| _                    => id
+
+end CollectFVars
+
+def collectFVars (s : CollectFVars.State) (e : Expr) : CollectFVars.State :=
+CollectFVars.main e s
+
+end Lean

stage0/src/Init/Lean/Util/CollectLevelParams.lean

@@ -15,47 +15,42 @@ structure State :=
 (visitedExpr  : ExprSet    := {})
 (params       : Array Name := #[])
 
-abbrev M := StateM State
+instance State.inhabited : Inhabited State := ⟨{}⟩
 
-@[inline] def visitLevel (f : Level → M Unit) (u : Level) : M Unit :=
-if !u.hasParam then pure ()
-else do
-  s ← get;
-  if s.visitedLevel.contains u then pure ()
-  else do
-    modify $ fun s => { visitedLevel := s.visitedLevel.insert u, .. s };
-    f u
+abbrev Visitor := State → State
 
-partial def collect : Level → M Unit
+@[inline] def visitLevel (f : Level → Visitor) (u : Level) : Visitor :=
+fun s =>
+  if !u.hasParam || s.visitedLevel.contains u then s
+  else f u { visitedLevel := s.visitedLevel.insert u, .. s }
+
+partial def collect : Level → Visitor
 | Level.succ v _    => visitLevel collect v
-| Level.max u v _   => do visitLevel collect u; visitLevel collect v
-| Level.imax u v _  => do visitLevel collect u; visitLevel collect v
-| Level.param n _   => modify $ fun s => { params := s.params.push n, .. s }
-| _                 => pure ()
+| Level.max u v _   => visitLevel collect v ∘ visitLevel collect u
+| Level.imax u v _  => visitLevel collect v ∘ visitLevel collect u
+| Level.param n _   => fun s => { params := s.params.push n, .. s }
+| _                 => id
 
-@[inline] def visitExpr (f : Expr → M Unit) (e : Expr) : M Unit :=
-if !e.hasLevelParam then pure ()
-else do
-  s ← get;
-  if s.visitedExpr.contains e then pure ()
-  else do
-    modify $ fun s => { visitedExpr := s.visitedExpr.insert e, .. s };
-    f e
+@[inline] def visitExpr (f : Expr → Visitor) (e : Expr) : Visitor :=
+fun s =>
+  if !e.hasLevelParam then s
+  else if s.visitedExpr.contains e then s
+  else f e { visitedExpr := s.visitedExpr.insert e, .. s }
 
-partial def main : Expr → M Unit
+partial def main : Expr → Visitor
 | Expr.proj _ _ s _    => visitExpr main s
-| Expr.forallE _ d b _ => do visitExpr main d; visitExpr main b
-| Expr.lam _ d b _     => do visitExpr main d; visitExpr main b
-| Expr.letE _ t v b _  => do visitExpr main t; visitExpr main v; visitExpr main b
-| Expr.app f a _       => do visitExpr main f; visitExpr main a
+| Expr.forallE _ d b _ => visitExpr main b ∘ visitExpr main d
+| Expr.lam _ d b _     => visitExpr main b ∘ visitExpr main d
+| Expr.letE _ t v b _  => visitExpr main b ∘ visitExpr main v ∘ visitExpr main t
+| Expr.app f a _       => visitExpr main a ∘ visitExpr main f
 | Expr.mdata _ b _     => visitExpr main b
-| Expr.const _ us _    => us.forM (visitLevel collect)
+| Expr.const _ us _    => fun s => us.foldl (fun s u => visitLevel collect u s) s
 | Expr.sort u _        => visitLevel collect u
-| _                    => pure ()
+| _                    => id
 
 end CollectLevelParams
 
-def collectLevelParams (e : Expr) : Array Name :=
-(CollectLevelParams.main e {}).2.params
+def collectLevelParams (s : CollectLevelParams.State) (e : Expr) : CollectLevelParams.State :=
+CollectLevelParams.main e s
 
 end Lean

stage0/stdlib/Init/Lean/Elab/DeclModifiers.c

@@ -19,7 +19,6 @@ extern lean_object* l_Lean_List_format___rarg___closed__4;
 lean_object* l_Lean_Syntax_foldArgsAuxM___main___at_Lean_Elab_Command_elabAttrs___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_Modifiers_hasFormat___closed__6;
 lean_object* l_Lean_Syntax_getOptional_x3f(lean_object*);
-lean_object* l_Lean_Elab_throwError___at_Lean_Elab_Command_elabCommand___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Format_pretty(lean_object*, lean_object*);
 lean_object* l_List_map___main___at_Lean_Elab_Command_Modifiers_hasFormat___spec__2(lean_object*);
 lean_object* l_Lean_fmt___at_Lean_Elab_Command_Modifiers_hasFormat___spec__1(lean_object*);
@@ -42,33 +41,29 @@ lean_object* lean_string_utf8_extract(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_applyAttributes(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
 lean_object* lean_string_utf8_byte_size(lean_object*);
 lean_object* l_Lean_Elab_Command_Modifiers_hasFormat(lean_object*);
-lean_object* l_Lean_Elab_throwError___at_Lean_Elab_Command_elabAttr___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_Modifiers_hasFormat___closed__11;
 lean_object* l_Lean_Elab_Command_mkDeclName(lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_AttributeApplicationTime_beq(uint8_t, uint8_t);
 lean_object* l_Lean_Elab_Command_Modifiers_hasFormat___closed__4;
-lean_object* l_Lean_Elab_mkMessage___at_Lean_Elab_Command_elabCommand___spec__2(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_fget(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_Visibility_hasToString(uint8_t);
 lean_object* l_Lean_Elab_Command_getCurrNamespace(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_Modifiers_hasToString;
 lean_object* lean_nat_sub(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_Modifiers_hasToString___lambda__1___boxed(lean_object*);
-lean_object* l_Lean_Elab_throwError___at_Lean_Elab_Command_elabModifiers___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Name_append___main(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabModifiers___closed__4;
 lean_object* l_Lean_Elab_Command_Modifiers_hasFormat___closed__9;
 extern lean_object* l_Lean_Format_join___closed__1;
-lean_object* l_Lean_Elab_throwError___at_Lean_Elab_Command_elabModifiers___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_Modifiers_hasFormat___closed__13;
 lean_object* l___private_Init_Lean_Elab_Command_1__ioErrorToMessage(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_Visibility_hasToString___boxed(lean_object*);
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_Modifiers_hasToString___lambda__1(lean_object*);
-lean_object* l_Lean_Elab_throwError___at_Lean_Elab_Command_elabModifiers___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l___regBuiltinParser_Lean_Parser_Command_antiquot___closed__2;
 lean_object* l_Function_comp___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Command_throwError___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Options_empty;
 extern lean_object* l_Lean_Parser_Command_attributes___elambda__1___closed__5;
 lean_object* l_Lean_Elab_Command_elabModifiers___closed__1;
@@ -77,7 +72,6 @@ lean_object* l_Lean_Elab_Command_elabModifiers___closed__2;
 lean_object* l_Lean_Elab_Command_elabAttr___closed__6;
 lean_object* l_Lean_Elab_Command_elabAttrs(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabAttr___closed__1;
-lean_object* l_Lean_Elab_Command_elabAttr___boxed(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Command_docComment___elambda__1___closed__5;
 lean_object* l_Lean_Elab_Command_Modifiers_hasToString___closed__2;
 lean_object* l_Lean_Elab_Command_Modifiers_hasFormat___closed__12;
@@ -121,12 +115,10 @@ lean_object* l_Lean_Elab_Command_Attribute_hasFormat(lean_object*);
 extern lean_object* l_Lean_Parser_Command_private___elambda__1___closed__2;
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Command_partial___elambda__1___closed__1;
-lean_object* l_Lean_Elab_throwError___at_Lean_Elab_Command_elabAttr___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_formatStxAux___main(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabModifiers___closed__7;
 lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabAttr(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_throwError___at_Lean_Elab_Command_elabModifiers___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_getAttributeImpl(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabModifiers___closed__5;
 extern lean_object* l_addParenHeuristic___closed__1;
@@ -1070,33 +1062,6 @@ lean_dec(x_1);
 return x_2;
 }
 }
-lean_object* l_Lean_Elab_throwError___at_Lean_Elab_Command_elabAttr___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
-_start:
-{
-uint8_t x_5; lean_object* x_6; uint8_t x_7; 
-x_5 = 2;
-x_6 = l_Lean_Elab_mkMessage___at_Lean_Elab_Command_elabCommand___spec__2(x_2, x_5, x_1, x_3, x_4);
-x_7 = !lean_is_exclusive(x_6);
-if (x_7 == 0)
-{
-lean_ctor_set_tag(x_6, 1);
-return x_6;
-}
-else
-{
-lean_object* x_8; lean_object* x_9; lean_object* x_10; 
-x_8 = lean_ctor_get(x_6, 0);
-x_9 = lean_ctor_get(x_6, 1);
-lean_inc(x_9);
-lean_inc(x_8);
-lean_dec(x_6);
-x_10 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_10, 0, x_8);
-lean_ctor_set(x_10, 1, x_9);
-return x_10;
-}
-}
-}
 lean_object* _init_l_Lean_Elab_Command_elabAttr___closed__1() {
 _start:
 {
@@ -1156,17 +1121,16 @@ return x_2;
 lean_object* l_Lean_Elab_Command_elabAttr(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
-lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_40; 
-x_4 = lean_unsigned_to_nat(0u);
-x_5 = l_Lean_Syntax_getArg(x_1, x_4);
-x_40 = l_Lean_Syntax_isIdOrAtom_x3f(x_5);
+lean_object* x_4; lean_object* x_5; lean_object* x_38; lean_object* x_39; lean_object* x_40; 
+x_38 = lean_unsigned_to_nat(0u);
+x_39 = l_Lean_Syntax_getArg(x_1, x_38);
+x_40 = l_Lean_Syntax_isIdOrAtom_x3f(x_39);
 if (lean_obj_tag(x_40) == 0)
 {
 lean_object* x_41; lean_object* x_42; uint8_t x_43; 
+lean_dec(x_1);
 x_41 = l_Lean_Elab_Command_elabAttr___closed__6;
-x_42 = l_Lean_Elab_throwError___at_Lean_Elab_Command_elabAttr___spec__1(x_5, x_41, x_2, x_3);
-lean_dec(x_2);
-lean_dec(x_5);
+x_42 = l_Lean_Elab_Command_throwError___rarg(x_39, x_41, x_2, x_3);
 x_43 = !lean_is_exclusive(x_42);
 if (x_43 == 0)
 {
@@ -1189,149 +1153,133 @@ return x_46;
 else
 {
 lean_object* x_47; lean_object* x_48; lean_object* x_49; 
-lean_dec(x_5);
+lean_dec(x_39);
 x_47 = lean_ctor_get(x_40, 0);
 lean_inc(x_47);
 lean_dec(x_40);
 x_48 = lean_box(0);
 x_49 = lean_name_mk_string(x_48, x_47);
-x_6 = x_49;
-x_7 = x_3;
-goto block_39;
+x_4 = x_49;
+x_5 = x_3;
+goto block_37;
 }
-block_39:
+block_37:
 {
-lean_object* x_8; 
-lean_inc(x_6);
-x_8 = lean_is_attribute(x_6, x_7);
-if (lean_obj_tag(x_8) == 0)
+lean_object* x_6; 
+lean_inc(x_4);
+x_6 = lean_is_attribute(x_4, x_5);
+if (lean_obj_tag(x_6) == 0)
 {
-lean_object* x_9; uint8_t x_10; 
-x_9 = lean_ctor_get(x_8, 0);
+lean_object* x_7; uint8_t x_8; 
+x_7 = lean_ctor_get(x_6, 0);
+lean_inc(x_7);
+x_8 = lean_unbox(x_7);
+lean_dec(x_7);
+if (x_8 == 0)
+{
+lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16; 
+x_9 = lean_ctor_get(x_6, 1);
 lean_inc(x_9);
-x_10 = lean_unbox(x_9);
-lean_dec(x_9);
-if (x_10 == 0)
-{
-lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; 
-x_11 = lean_ctor_get(x_8, 1);
-lean_inc(x_11);
-lean_dec(x_8);
-x_12 = lean_alloc_ctor(4, 1, 0);
-lean_ctor_set(x_12, 0, x_6);
-x_13 = l_Lean_Elab_Command_elabAttr___closed__3;
-x_14 = lean_alloc_ctor(8, 2, 0);
-lean_ctor_set(x_14, 0, x_13);
-lean_ctor_set(x_14, 1, x_12);
-x_15 = l_Lean_MessageData_arrayExpr_toMessageData___main___closed__1;
-x_16 = lean_alloc_ctor(8, 2, 0);
-lean_ctor_set(x_16, 0, x_14);
-lean_ctor_set(x_16, 1, x_15);
-x_17 = l_Lean_Elab_throwError___at_Lean_Elab_Command_elabCommand___spec__1(x_1, x_16, x_2, x_11);
-lean_dec(x_2);
-x_18 = !lean_is_exclusive(x_17);
-if (x_18 == 0)
-{
-return x_17;
-}
-else
-{
-lean_object* x_19; lean_object* x_20; lean_object* x_21; 
-x_19 = lean_ctor_get(x_17, 0);
-x_20 = lean_ctor_get(x_17, 1);
-lean_inc(x_20);
-lean_inc(x_19);
-lean_dec(x_17);
-x_21 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_21, 0, x_19);
-lean_ctor_set(x_21, 1, x_20);
-return x_21;
-}
-}
-else
-{
-uint8_t x_22; 
-lean_dec(x_2);
-x_22 = !lean_is_exclusive(x_8);
-if (x_22 == 0)
-{
-lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; 
-x_23 = lean_ctor_get(x_8, 0);
-lean_dec(x_23);
-x_24 = lean_unsigned_to_nat(1u);
-x_25 = l_Lean_Syntax_getArg(x_1, x_24);
-x_26 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_26, 0, x_6);
-lean_ctor_set(x_26, 1, x_25);
-lean_ctor_set(x_8, 0, x_26);
-return x_8;
-}
-else
-{
-lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; 
-x_27 = lean_ctor_get(x_8, 1);
-lean_inc(x_27);
-lean_dec(x_8);
-x_28 = lean_unsigned_to_nat(1u);
-x_29 = l_Lean_Syntax_getArg(x_1, x_28);
-x_30 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_30, 0, x_6);
-lean_ctor_set(x_30, 1, x_29);
-x_31 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_31, 0, x_30);
-lean_ctor_set(x_31, 1, x_27);
-return x_31;
-}
-}
-}
-else
-{
-uint8_t x_32; 
 lean_dec(x_6);
-x_32 = !lean_is_exclusive(x_8);
-if (x_32 == 0)
+x_10 = lean_alloc_ctor(4, 1, 0);
+lean_ctor_set(x_10, 0, x_4);
+x_11 = l_Lean_Elab_Command_elabAttr___closed__3;
+x_12 = lean_alloc_ctor(8, 2, 0);
+lean_ctor_set(x_12, 0, x_11);
+lean_ctor_set(x_12, 1, x_10);
+x_13 = l_Lean_MessageData_arrayExpr_toMessageData___main___closed__1;
+x_14 = lean_alloc_ctor(8, 2, 0);
+lean_ctor_set(x_14, 0, x_12);
+lean_ctor_set(x_14, 1, x_13);
+x_15 = l_Lean_Elab_Command_throwError___rarg(x_1, x_14, x_2, x_9);
+x_16 = !lean_is_exclusive(x_15);
+if (x_16 == 0)
 {
-lean_object* x_33; lean_object* x_34; 
-x_33 = lean_ctor_get(x_8, 0);
-x_34 = l___private_Init_Lean_Elab_Command_1__ioErrorToMessage(x_2, x_1, x_33);
-lean_ctor_set(x_8, 0, x_34);
-return x_8;
+return x_15;
 }
 else
 {
-lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; 
-x_35 = lean_ctor_get(x_8, 0);
-x_36 = lean_ctor_get(x_8, 1);
-lean_inc(x_36);
-lean_inc(x_35);
-lean_dec(x_8);
-x_37 = l___private_Init_Lean_Elab_Command_1__ioErrorToMessage(x_2, x_1, x_35);
-x_38 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_38, 0, x_37);
-lean_ctor_set(x_38, 1, x_36);
-return x_38;
+lean_object* x_17; lean_object* x_18; lean_object* x_19; 
+x_17 = lean_ctor_get(x_15, 0);
+x_18 = lean_ctor_get(x_15, 1);
+lean_inc(x_18);
+lean_inc(x_17);
+lean_dec(x_15);
+x_19 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_19, 0, x_17);
+lean_ctor_set(x_19, 1, x_18);
+return x_19;
 }
 }
-}
-}
-}
-lean_object* l_Lean_Elab_throwError___at_Lean_Elab_Command_elabAttr___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
-_start:
+else
 {
-lean_object* x_5; 
-x_5 = l_Lean_Elab_throwError___at_Lean_Elab_Command_elabAttr___spec__1(x_1, x_2, x_3, x_4);
-lean_dec(x_3);
-lean_dec(x_1);
-return x_5;
-}
-}
-lean_object* l_Lean_Elab_Command_elabAttr___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
+uint8_t x_20; 
+lean_dec(x_2);
+x_20 = !lean_is_exclusive(x_6);
+if (x_20 == 0)
 {
-lean_object* x_4; 
-x_4 = l_Lean_Elab_Command_elabAttr(x_1, x_2, x_3);
+lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; 
+x_21 = lean_ctor_get(x_6, 0);
+lean_dec(x_21);
+x_22 = lean_unsigned_to_nat(1u);
+x_23 = l_Lean_Syntax_getArg(x_1, x_22);
 lean_dec(x_1);
-return x_4;
+x_24 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_24, 0, x_4);
+lean_ctor_set(x_24, 1, x_23);
+lean_ctor_set(x_6, 0, x_24);
+return x_6;
+}
+else
+{
+lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; 
+x_25 = lean_ctor_get(x_6, 1);
+lean_inc(x_25);
+lean_dec(x_6);
+x_26 = lean_unsigned_to_nat(1u);
+x_27 = l_Lean_Syntax_getArg(x_1, x_26);
+lean_dec(x_1);
+x_28 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_28, 0, x_4);
+lean_ctor_set(x_28, 1, x_27);
+x_29 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_29, 0, x_28);
+lean_ctor_set(x_29, 1, x_25);
+return x_29;
+}
+}
+}
+else
+{
+uint8_t x_30; 
+lean_dec(x_4);
+x_30 = !lean_is_exclusive(x_6);
+if (x_30 == 0)
+{
+lean_object* x_31; lean_object* x_32; 
+x_31 = lean_ctor_get(x_6, 0);
+x_32 = l___private_Init_Lean_Elab_Command_1__ioErrorToMessage(x_2, x_1, x_31);
+lean_dec(x_1);
+lean_ctor_set(x_6, 0, x_32);
+return x_6;
+}
+else
+{
+lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; 
+x_33 = lean_ctor_get(x_6, 0);
+x_34 = lean_ctor_get(x_6, 1);
+lean_inc(x_34);
+lean_inc(x_33);
+lean_dec(x_6);
+x_35 = l___private_Init_Lean_Elab_Command_1__ioErrorToMessage(x_2, x_1, x_33);
+lean_dec(x_1);
+x_36 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_36, 0, x_35);
+lean_ctor_set(x_36, 1, x_34);
+return x_36;
+}
+}
+}
 }
 }
 lean_object* l_Lean_Syntax_foldArgsAuxM___main___at_Lean_Elab_Command_elabAttrs___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) {
@@ -1357,7 +1305,6 @@ lean_object* x_10; lean_object* x_11;
 x_10 = lean_array_fget(x_2, x_3);
 lean_inc(x_5);
 x_11 = l_Lean_Elab_Command_elabAttr(x_10, x_5, x_6);
-lean_dec(x_10);
 if (lean_obj_tag(x_11) == 0)
 {
 lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
@@ -1437,60 +1384,6 @@ lean_dec(x_1);
 return x_4;
 }
 }
-lean_object* l_Lean_Elab_throwError___at_Lean_Elab_Command_elabModifiers___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
-_start:
-{
-uint8_t x_5; lean_object* x_6; uint8_t x_7; 
-x_5 = 2;
-x_6 = l_Lean_Elab_mkMessage___at_Lean_Elab_Command_elabCommand___spec__2(x_2, x_5, x_1, x_3, x_4);
-x_7 = !lean_is_exclusive(x_6);
-if (x_7 == 0)
-{
-lean_ctor_set_tag(x_6, 1);
-return x_6;
-}
-else
-{
-lean_object* x_8; lean_object* x_9; lean_object* x_10; 
-x_8 = lean_ctor_get(x_6, 0);
-x_9 = lean_ctor_get(x_6, 1);
-lean_inc(x_9);
-lean_inc(x_8);
-lean_dec(x_6);
-x_10 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_10, 0, x_8);
-lean_ctor_set(x_10, 1, x_9);
-return x_10;
-}
-}
-}
-lean_object* l_Lean_Elab_throwError___at_Lean_Elab_Command_elabModifiers___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
-_start:
-{
-uint8_t x_5; lean_object* x_6; uint8_t x_7; 
-x_5 = 2;
-x_6 = l_Lean_Elab_mkMessage___at_Lean_Elab_Command_elabCommand___spec__2(x_2, x_5, x_1, x_3, x_4);
-x_7 = !lean_is_exclusive(x_6);
-if (x_7 == 0)
-{
-lean_ctor_set_tag(x_6, 1);
-return x_6;
-}
-else
-{
-lean_object* x_8; lean_object* x_9; lean_object* x_10; 
-x_8 = lean_ctor_get(x_6, 0);
-x_9 = lean_ctor_get(x_6, 1);
-lean_inc(x_9);
-lean_inc(x_8);
-lean_dec(x_6);
-x_10 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_10, 0, x_8);
-lean_ctor_set(x_10, 1, x_9);
-return x_10;
-}
-}
-}
 lean_object* _init_l_Lean_Elab_Command_elabModifiers___closed__1() {
 _start:
 {
@@ -1641,9 +1534,7 @@ x_96 = l_Lean_Elab_Command_elabModifiers___closed__7;
 x_97 = lean_alloc_ctor(8, 2, 0);
 lean_ctor_set(x_97, 0, x_96);
 lean_ctor_set(x_97, 1, x_95);
-x_98 = l_Lean_Elab_throwError___at_Lean_Elab_Command_elabModifiers___spec__2(x_87, x_97, x_2, x_3);
-lean_dec(x_2);
-lean_dec(x_87);
+x_98 = l_Lean_Elab_Command_throwError___rarg(x_87, x_97, x_2, x_3);
 x_99 = !lean_is_exclusive(x_98);
 if (x_99 == 0)
 {
@@ -1720,9 +1611,7 @@ x_119 = l_Lean_Elab_Command_elabModifiers___closed__7;
 x_120 = lean_alloc_ctor(8, 2, 0);
 lean_ctor_set(x_120, 0, x_119);
 lean_ctor_set(x_120, 1, x_118);
-x_121 = l_Lean_Elab_throwError___at_Lean_Elab_Command_elabModifiers___spec__2(x_110, x_120, x_2, x_3);
-lean_dec(x_2);
-lean_dec(x_110);
+x_121 = l_Lean_Elab_Command_throwError___rarg(x_110, x_120, x_2, x_3);
 x_122 = lean_ctor_get(x_121, 0);
 lean_inc(x_122);
 x_123 = lean_ctor_get(x_121, 1);
@@ -1784,9 +1673,7 @@ lean_dec(x_13);
 lean_dec(x_11);
 lean_dec(x_7);
 x_75 = l_Lean_Elab_Command_elabModifiers___closed__4;
-x_76 = l_Lean_Elab_throwError___at_Lean_Elab_Command_elabModifiers___spec__1(x_69, x_75, x_2, x_17);
-lean_dec(x_2);
-lean_dec(x_69);
+x_76 = l_Lean_Elab_Command_throwError___rarg(x_69, x_75, x_2, x_17);
 x_77 = !lean_is_exclusive(x_76);
 if (x_77 == 0)
 {
@@ -2054,26 +1941,6 @@ return x_54;
 }
 }
 }
-lean_object* l_Lean_Elab_throwError___at_Lean_Elab_Command_elabModifiers___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
-_start:
-{
-lean_object* x_5; 
-x_5 = l_Lean_Elab_throwError___at_Lean_Elab_Command_elabModifiers___spec__1(x_1, x_2, x_3, x_4);
-lean_dec(x_3);
-lean_dec(x_1);
-return x_5;
-}
-}
-lean_object* l_Lean_Elab_throwError___at_Lean_Elab_Command_elabModifiers___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
-_start:
-{
-lean_object* x_5; 
-x_5 = l_Lean_Elab_throwError___at_Lean_Elab_Command_elabModifiers___spec__2(x_1, x_2, x_3, x_4);
-lean_dec(x_3);
-lean_dec(x_1);
-return x_5;
-}
-}
 lean_object* l_Lean_Elab_Command_elabModifiers___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {

stage0/stdlib/Init/Lean/Elab/Declaration.c

@@ -15,8 +15,8 @@ extern "C" {
 #endif
 lean_object* l_Lean_Elab_Command_elabDeclaration(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabConstant___closed__9;
+lean_object* l___private_Init_Lean_Elab_Command_13__addScopes___main(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkForall(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l___private_Init_Lean_Elab_Command_10__addScopes___main(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Command_abbrev___elambda__1___closed__2;
 lean_object* l_Lean_Elab_Command_addDecl(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -26,7 +26,6 @@ lean_object* l_unreachable_x21___rarg(lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Command_elabAxiom___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclaration(lean_object*);
 lean_object* l_Lean_Syntax_getOptional_x3f(lean_object*);
-lean_object* l_Lean_Elab_throwError___at_Lean_Elab_Command_elabCommand___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Meta_mkEqTrans___closed__3;
 lean_object* l_Lean_Elab_Command_elabConstant___closed__2;
 lean_object* l_Lean_Elab_Command_elabDeclaration___closed__4;
@@ -44,14 +43,13 @@ lean_object* l_Lean_Elab_Command_elabExample___closed__2;
 uint8_t lean_name_eq(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Command_declaration___elambda__1___closed__2;
 lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*);
-lean_object* l___private_Init_Lean_Elab_Command_7__getVarDecls(lean_object*);
 lean_object* lean_array_push(lean_object*, lean_object*);
+lean_object* l___private_Init_Lean_Elab_Command_10__getVarDecls(lean_object*);
 lean_object* lean_array_get_size(lean_object*);
 lean_object* l_Lean_Elab_Term_mkForallUsedOnly(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclaration___closed__2;
 lean_object* lean_string_utf8_byte_size(lean_object*);
 extern lean_object* l_Lean_Parser_Command_example___elambda__1___closed__2;
-lean_object* l_Lean_Elab_Command_elabAxiom___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Name_getNumParts___main(lean_object*);
 lean_object* l_Lean_Elab_Command_elabInductive___rarg(lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
@@ -60,7 +58,6 @@ extern lean_object* l_Lean_Parser_Command_classInductive___elambda__1___closed__
 lean_object* l_Lean_Elab_Command_mkDeclName(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclaration___closed__1;
 lean_object* l_Lean_Elab_Command_expandOptDeclSig___boxed(lean_object*);
-lean_object* l_Lean_Elab_mkMessage___at_Lean_Elab_Command_elabCommand___spec__2(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_fget(lean_object*, lean_object*);
 extern lean_object* l_Lean_Name_appendIndexAfter___closed__1;
 lean_object* l_Lean_Elab_Term_levelMVarToParam(lean_object*, lean_object*, lean_object*);
@@ -75,6 +72,7 @@ lean_object* l_Lean_Elab_Command_elabConstant(lean_object*, lean_object*, lean_o
 lean_object* l_Lean_Elab_Command_elabAxiom___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_expandOptDeclSig(lean_object*);
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclaration___closed__3;
+extern lean_object* l_Lean_Elab_Command_mkDef___lambda__1___closed__1;
 extern lean_object* l_Lean_Meta_registerInstanceAttr___closed__2;
 lean_object* l_Lean_Syntax_getId(lean_object*);
 lean_object* l_Lean_Elab_Command_elabClassInductive(lean_object*, lean_object*, lean_object*);
@@ -82,6 +80,7 @@ lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_elabAxiom___spec__4(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Command_namespace___elambda__1___closed__1;
 extern lean_object* l___regBuiltinParser_Lean_Parser_Command_antiquot___closed__2;
+lean_object* l_Lean_Elab_Command_throwError___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabConstant___closed__7;
 lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_elabAxiom___spec__3(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_hole___elambda__1___closed__1;
@@ -124,8 +123,6 @@ lean_object* l_Lean_Elab_Command_throwAlreadyDeclaredUniverseLevel___rarg(lean_o
 lean_object* l_Lean_Elab_Command_elabDefLike(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_foldArgsAuxM___main___at_Lean_Syntax_foldSepRevArgsM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_expandDeclSig___boxed(lean_object*);
-lean_object* l_Lean_Elab_throwError___at_Lean_Elab_Command_elabInstance___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Command_elabDeclaration___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_elabBinders___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l___private_Init_Lean_Elab_Term_8__expandCDot___closed__5;
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
@@ -133,7 +130,6 @@ lean_object* l_Lean_Elab_Command_elabDeclaration___closed__2;
 lean_object* l_Lean_Elab_Command_elabAxiom___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabConstant___closed__5;
 lean_object* l_Lean_Elab_Command_elabInductive(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_collectLevelParams(lean_object*);
 lean_object* l_Lean_Elab_Command_elabDeclaration___closed__1;
 lean_object* l___private_Init_Lean_Elab_Term_19__synthesizeSyntheticMVarsAux___main(uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabDeclaration___closed__3;
@@ -141,16 +137,16 @@ lean_object* l_Lean_Elab_Command_elabConstant___closed__3;
 lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_elabAxiom___spec__2(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabAbbrev___closed__1;
 lean_object* l_Lean_Elab_Command_elabAbbrev___closed__4;
+lean_object* l_Lean_CollectLevelParams_main___main(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_elabAxiom___spec__1(lean_object*, lean_object*, lean_object*);
 lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Command_constant___elambda__1___closed__2;
-lean_object* l___private_Init_Lean_Elab_Command_5__mkTermContext(lean_object*, lean_object*);
+lean_object* l___private_Init_Lean_Elab_Command_9__mkTermState(lean_object*);
 lean_object* l_Lean_Elab_Command_elabConstant___closed__8;
 extern lean_object* l_Lean_Parser_Command_theorem___elambda__1___closed__2;
 lean_object* l_Lean_Elab_Command_elabClassInductive___rarg(lean_object*);
 lean_object* l___private_Init_Lean_Elab_Command_3__setState(lean_object*, lean_object*, lean_object*);
-lean_object* l___private_Init_Lean_Elab_Command_6__mkTermState(lean_object*);
-lean_object* l_Lean_Elab_throwError___at_Lean_Elab_Command_elabInstance___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l___private_Init_Lean_Elab_Command_8__mkTermContext(lean_object*, lean_object*);
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Command_declId___elambda__1___closed__2;
 lean_object* l_Lean_Elab_Command_expandOptDeclSig(lean_object* x_1) {
@@ -574,33 +570,6 @@ return x_52;
 }
 }
 }
-lean_object* l_Lean_Elab_throwError___at_Lean_Elab_Command_elabInstance___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
-_start:
-{
-uint8_t x_5; lean_object* x_6; uint8_t x_7; 
-x_5 = 2;
-x_6 = l_Lean_Elab_mkMessage___at_Lean_Elab_Command_elabCommand___spec__2(x_2, x_5, x_1, x_3, x_4);
-x_7 = !lean_is_exclusive(x_6);
-if (x_7 == 0)
-{
-lean_ctor_set_tag(x_6, 1);
-return x_6;
-}
-else
-{
-lean_object* x_8; lean_object* x_9; lean_object* x_10; 
-x_8 = lean_ctor_get(x_6, 0);
-x_9 = lean_ctor_get(x_6, 1);
-lean_inc(x_9);
-lean_inc(x_8);
-lean_dec(x_6);
-x_10 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_10, 0, x_8);
-lean_ctor_set(x_10, 1, x_9);
-return x_10;
-}
-}
-}
 lean_object* _init_l_Lean_Elab_Command_elabInstance___closed__1() {
 _start:
 {
@@ -639,9 +608,7 @@ lean_dec(x_11);
 lean_dec(x_9);
 lean_dec(x_8);
 x_15 = l___private_Init_Lean_Elab_Term_16__synthesizeSyntheticMVar___closed__3;
-x_16 = l_Lean_Elab_throwError___at_Lean_Elab_Command_elabInstance___spec__1(x_2, x_15, x_3, x_4);
-lean_dec(x_3);
-lean_dec(x_2);
+x_16 = l_Lean_Elab_Command_throwError___rarg(x_2, x_15, x_3, x_4);
 x_17 = !lean_is_exclusive(x_16);
 if (x_17 == 0)
 {
@@ -709,16 +676,6 @@ return x_34;
 }
 }
 }
-lean_object* l_Lean_Elab_throwError___at_Lean_Elab_Command_elabInstance___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
-_start:
-{
-lean_object* x_5; 
-x_5 = l_Lean_Elab_throwError___at_Lean_Elab_Command_elabInstance___spec__1(x_1, x_2, x_3, x_4);
-lean_dec(x_3);
-lean_dec(x_1);
-return x_5;
-}
-}
 lean_object* _init_l_Lean_Elab_Command_elabExample___closed__1() {
 _start:
 {
@@ -2951,6 +2908,7 @@ lean_dec(x_7);
 if (x_8 == 0)
 {
 lean_object* x_9; 
+lean_dec(x_5);
 lean_dec(x_3);
 x_9 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_9, 0, x_4);
@@ -2983,7 +2941,6 @@ lean_object* x_17; uint8_t x_18;
 lean_dec(x_12);
 lean_dec(x_4);
 x_17 = l_Lean_Elab_Command_throwAlreadyDeclaredUniverseLevel___rarg(x_10, x_13, x_5, x_6);
-lean_dec(x_10);
 x_18 = !lean_is_exclusive(x_17);
 if (x_18 == 0)
 {
@@ -3066,98 +3023,78 @@ x_26 = l_Lean_Elab_Term_levelMVarToParam(x_25, x_7, x_24);
 x_27 = !lean_is_exclusive(x_26);
 if (x_27 == 0)
 {
-lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; uint8_t x_32; lean_object* x_33; lean_object* x_34; 
+lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; uint8_t x_34; lean_object* x_35; lean_object* x_36; 
 x_28 = lean_ctor_get(x_26, 0);
+x_29 = l_Lean_Elab_Command_mkDef___lambda__1___closed__1;
 lean_inc(x_28);
-x_29 = l_Lean_collectLevelParams(x_28);
-x_30 = l_Lean_Elab_Command_sortDeclLevelParams(x_3, x_29);
-x_31 = lean_alloc_ctor(0, 3, 0);
-lean_ctor_set(x_31, 0, x_4);
-lean_ctor_set(x_31, 1, x_30);
-lean_ctor_set(x_31, 2, x_28);
-x_32 = lean_ctor_get_uint8(x_5, sizeof(void*)*2 + 3);
-x_33 = lean_alloc_ctor(0, 1, 1);
-lean_ctor_set(x_33, 0, x_31);
-lean_ctor_set_uint8(x_33, sizeof(void*)*1, x_32);
-x_34 = lean_alloc_ctor(0, 1, 0);
-lean_ctor_set(x_34, 0, x_33);
-lean_ctor_set(x_26, 0, x_34);
+x_30 = l_Lean_CollectLevelParams_main___main(x_28, x_29);
+x_31 = lean_ctor_get(x_30, 2);
+lean_inc(x_31);
+lean_dec(x_30);
+x_32 = l_Lean_Elab_Command_sortDeclLevelParams(x_3, x_31);
+x_33 = lean_alloc_ctor(0, 3, 0);
+lean_ctor_set(x_33, 0, x_4);
+lean_ctor_set(x_33, 1, x_32);
+lean_ctor_set(x_33, 2, x_28);
+x_34 = lean_ctor_get_uint8(x_5, sizeof(void*)*2 + 3);
+x_35 = lean_alloc_ctor(0, 1, 1);
+lean_ctor_set(x_35, 0, x_33);
+lean_ctor_set_uint8(x_35, sizeof(void*)*1, x_34);
+x_36 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_36, 0, x_35);
+lean_ctor_set(x_26, 0, x_36);
 return x_26;
 }
 else
 {
-lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; uint8_t x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; 
-x_35 = lean_ctor_get(x_26, 0);
-x_36 = lean_ctor_get(x_26, 1);
-lean_inc(x_36);
-lean_inc(x_35);
+lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; uint8_t x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; 
+x_37 = lean_ctor_get(x_26, 0);
+x_38 = lean_ctor_get(x_26, 1);
+lean_inc(x_38);
+lean_inc(x_37);
 lean_dec(x_26);
-lean_inc(x_35);
-x_37 = l_Lean_collectLevelParams(x_35);
-x_38 = l_Lean_Elab_Command_sortDeclLevelParams(x_3, x_37);
-x_39 = lean_alloc_ctor(0, 3, 0);
-lean_ctor_set(x_39, 0, x_4);
-lean_ctor_set(x_39, 1, x_38);
-lean_ctor_set(x_39, 2, x_35);
-x_40 = lean_ctor_get_uint8(x_5, sizeof(void*)*2 + 3);
-x_41 = lean_alloc_ctor(0, 1, 1);
-lean_ctor_set(x_41, 0, x_39);
-lean_ctor_set_uint8(x_41, sizeof(void*)*1, x_40);
-x_42 = lean_alloc_ctor(0, 1, 0);
-lean_ctor_set(x_42, 0, x_41);
-x_43 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_43, 0, x_42);
-lean_ctor_set(x_43, 1, x_36);
-return x_43;
-}
-}
-else
-{
-uint8_t x_44; 
-lean_dec(x_7);
-lean_dec(x_4);
-lean_dec(x_3);
-x_44 = !lean_is_exclusive(x_22);
-if (x_44 == 0)
-{
-return x_22;
-}
-else
-{
-lean_object* x_45; lean_object* x_46; lean_object* x_47; 
-x_45 = lean_ctor_get(x_22, 0);
-x_46 = lean_ctor_get(x_22, 1);
-lean_inc(x_46);
-lean_inc(x_45);
-lean_dec(x_22);
-x_47 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_47, 0, x_45);
-lean_ctor_set(x_47, 1, x_46);
+x_39 = l_Lean_Elab_Command_mkDef___lambda__1___closed__1;
+lean_inc(x_37);
+x_40 = l_Lean_CollectLevelParams_main___main(x_37, x_39);
+x_41 = lean_ctor_get(x_40, 2);
+lean_inc(x_41);
+lean_dec(x_40);
+x_42 = l_Lean_Elab_Command_sortDeclLevelParams(x_3, x_41);
+x_43 = lean_alloc_ctor(0, 3, 0);
+lean_ctor_set(x_43, 0, x_4);
+lean_ctor_set(x_43, 1, x_42);
+lean_ctor_set(x_43, 2, x_37);
+x_44 = lean_ctor_get_uint8(x_5, sizeof(void*)*2 + 3);
+x_45 = lean_alloc_ctor(0, 1, 1);
+lean_ctor_set(x_45, 0, x_43);
+lean_ctor_set_uint8(x_45, sizeof(void*)*1, x_44);
+x_46 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_46, 0, x_45);
+x_47 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_47, 0, x_46);
+lean_ctor_set(x_47, 1, x_38);
 return x_47;
 }
 }
-}
 else
 {
 uint8_t x_48; 
 lean_dec(x_7);
 lean_dec(x_4);
 lean_dec(x_3);
-lean_dec(x_2);
-lean_dec(x_1);
-x_48 = !lean_is_exclusive(x_19);
+x_48 = !lean_is_exclusive(x_22);
 if (x_48 == 0)
 {
-return x_19;
+return x_22;
 }
 else
 {
 lean_object* x_49; lean_object* x_50; lean_object* x_51; 
-x_49 = lean_ctor_get(x_19, 0);
-x_50 = lean_ctor_get(x_19, 1);
+x_49 = lean_ctor_get(x_22, 0);
+x_50 = lean_ctor_get(x_22, 1);
 lean_inc(x_50);
 lean_inc(x_49);
-lean_dec(x_19);
+lean_dec(x_22);
 x_51 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_51, 0, x_49);
 lean_ctor_set(x_51, 1, x_50);
@@ -3168,26 +3105,24 @@ return x_51;
 else
 {
 uint8_t x_52; 
-lean_dec(x_10);
 lean_dec(x_7);
-lean_dec(x_6);
 lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_52 = !lean_is_exclusive(x_14);
+x_52 = !lean_is_exclusive(x_19);
 if (x_52 == 0)
 {
-return x_14;
+return x_19;
 }
 else
 {
 lean_object* x_53; lean_object* x_54; lean_object* x_55; 
-x_53 = lean_ctor_get(x_14, 0);
-x_54 = lean_ctor_get(x_14, 1);
+x_53 = lean_ctor_get(x_19, 0);
+x_54 = lean_ctor_get(x_19, 1);
 lean_inc(x_54);
 lean_inc(x_53);
-lean_dec(x_14);
+lean_dec(x_19);
 x_55 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_55, 0, x_53);
 lean_ctor_set(x_55, 1, x_54);
@@ -3198,29 +3133,59 @@ return x_55;
 else
 {
 uint8_t x_56; 
+lean_dec(x_10);
 lean_dec(x_7);
 lean_dec(x_6);
 lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_56 = !lean_is_exclusive(x_9);
+x_56 = !lean_is_exclusive(x_14);
 if (x_56 == 0)
 {
+return x_14;
+}
+else
+{
+lean_object* x_57; lean_object* x_58; lean_object* x_59; 
+x_57 = lean_ctor_get(x_14, 0);
+x_58 = lean_ctor_get(x_14, 1);
+lean_inc(x_58);
+lean_inc(x_57);
+lean_dec(x_14);
+x_59 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_59, 0, x_57);
+lean_ctor_set(x_59, 1, x_58);
+return x_59;
+}
+}
+}
+else
+{
+uint8_t x_60; 
+lean_dec(x_7);
+lean_dec(x_6);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+x_60 = !lean_is_exclusive(x_9);
+if (x_60 == 0)
+{
 return x_9;
 }
 else
 {
-lean_object* x_57; lean_object* x_58; lean_object* x_59; 
-x_57 = lean_ctor_get(x_9, 0);
-x_58 = lean_ctor_get(x_9, 1);
-lean_inc(x_58);
-lean_inc(x_57);
+lean_object* x_61; lean_object* x_62; lean_object* x_63; 
+x_61 = lean_ctor_get(x_9, 0);
+x_62 = lean_ctor_get(x_9, 1);
+lean_inc(x_62);
+lean_inc(x_61);
 lean_dec(x_9);
-x_59 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_59, 0, x_57);
-lean_ctor_set(x_59, 1, x_58);
-return x_59;
+x_63 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_63, 0, x_61);
+lean_ctor_set(x_63, 1, x_62);
+return x_63;
 }
 }
 }
@@ -3280,6 +3245,7 @@ lean_dec(x_202);
 x_204 = l_Array_empty___closed__1;
 x_205 = l_Lean_Syntax_foldArgsAuxM___main___at_Lean_Syntax_foldSepRevArgsM___spec__1(x_7, x_203, x_12, x_204);
 lean_dec(x_203);
+lean_inc(x_3);
 lean_inc(x_16);
 x_206 = l_Array_iterateMAux___main___at_Lean_Elab_Command_elabAxiom___spec__5(x_2, x_205, x_12, x_16, x_3, x_17);
 lean_dec(x_205);
@@ -3304,6 +3270,7 @@ lean_dec(x_11);
 lean_dec(x_10);
 lean_dec(x_6);
 lean_dec(x_3);
+lean_dec(x_2);
 lean_dec(x_1);
 x_209 = !lean_is_exclusive(x_206);
 if (x_209 == 0)
@@ -3347,8 +3314,7 @@ x_22 = l_Lean_Parser_Command_namespace___elambda__1___closed__1;
 x_23 = 1;
 lean_inc(x_3);
 lean_inc(x_20);
-x_24 = l___private_Init_Lean_Elab_Command_10__addScopes___main(x_6, x_22, x_23, x_20, x_3, x_19);
-lean_dec(x_6);
+x_24 = l___private_Init_Lean_Elab_Command_13__addScopes___main(x_6, x_22, x_23, x_20, x_3, x_19);
 if (lean_obj_tag(x_24) == 0)
 {
 lean_object* x_25; lean_object* x_26; 
@@ -3414,9 +3380,9 @@ lean_inc(x_120);
 x_121 = lean_ctor_get(x_119, 1);
 lean_inc(x_121);
 lean_dec(x_119);
-x_122 = l___private_Init_Lean_Elab_Command_7__getVarDecls(x_120);
-x_123 = l___private_Init_Lean_Elab_Command_5__mkTermContext(x_3, x_120);
-x_124 = l___private_Init_Lean_Elab_Command_6__mkTermState(x_120);
+x_122 = l___private_Init_Lean_Elab_Command_10__getVarDecls(x_120);
+x_123 = l___private_Init_Lean_Elab_Command_8__mkTermContext(x_3, x_120);
+x_124 = l___private_Init_Lean_Elab_Command_9__mkTermState(x_120);
 lean_dec(x_120);
 x_125 = l_Lean_Elab_Term_elabBinders___rarg(x_122, x_118, x_123, x_124);
 lean_dec(x_122);
@@ -3475,6 +3441,7 @@ lean_dec(x_126);
 lean_dec(x_45);
 lean_dec(x_43);
 lean_dec(x_20);
+lean_dec(x_2);
 x_139 = lean_ctor_get(x_137, 0);
 lean_inc(x_139);
 x_140 = lean_ctor_get(x_137, 1);
@@ -3517,6 +3484,7 @@ lean_dec(x_126);
 lean_dec(x_45);
 lean_dec(x_43);
 lean_dec(x_20);
+lean_dec(x_2);
 x_146 = lean_ctor_get(x_144, 0);
 lean_inc(x_146);
 x_147 = lean_ctor_get(x_144, 1);
@@ -3536,6 +3504,7 @@ lean_dec(x_126);
 lean_dec(x_45);
 lean_dec(x_43);
 lean_dec(x_20);
+lean_dec(x_2);
 x_148 = lean_ctor_get(x_128, 0);
 lean_inc(x_148);
 x_149 = lean_ctor_get(x_128, 1);
@@ -3557,6 +3526,7 @@ lean_object* x_151; lean_object* x_152; lean_object* x_153;
 lean_dec(x_45);
 lean_dec(x_43);
 lean_dec(x_20);
+lean_dec(x_2);
 x_151 = lean_ctor_get(x_125, 1);
 lean_inc(x_151);
 lean_dec(x_125);
@@ -3698,6 +3668,7 @@ lean_object* x_180; lean_object* x_181;
 lean_dec(x_45);
 lean_dec(x_43);
 lean_dec(x_20);
+lean_dec(x_2);
 x_180 = lean_ctor_get(x_177, 0);
 lean_inc(x_180);
 x_181 = lean_ctor_get(x_177, 1);
@@ -3717,6 +3688,7 @@ lean_dec(x_118);
 lean_dec(x_45);
 lean_dec(x_43);
 lean_dec(x_20);
+lean_dec(x_2);
 x_182 = lean_ctor_get(x_119, 0);
 lean_inc(x_182);
 x_183 = lean_ctor_get(x_119, 1);
@@ -3735,6 +3707,7 @@ lean_dec(x_43);
 lean_dec(x_20);
 lean_dec(x_11);
 lean_dec(x_10);
+lean_dec(x_2);
 lean_dec(x_1);
 x_184 = lean_ctor_get(x_115, 0);
 lean_inc(x_184);
@@ -3754,6 +3727,7 @@ lean_dec(x_43);
 lean_dec(x_20);
 lean_dec(x_11);
 lean_dec(x_10);
+lean_dec(x_2);
 lean_dec(x_1);
 x_186 = lean_ctor_get(x_113, 0);
 lean_inc(x_186);
@@ -3768,6 +3742,7 @@ block_111:
 {
 lean_object* x_48; 
 lean_inc(x_3);
+lean_inc(x_2);
 x_48 = l_Lean_Elab_Command_addDecl(x_2, x_46, x_3, x_47);
 lean_dec(x_46);
 if (lean_obj_tag(x_48) == 0)
@@ -3790,6 +3765,7 @@ x_53 = 1;
 lean_inc(x_3);
 x_54 = l_Array_forMAux___main___at_Lean_Elab_Command_applyAttributes___spec__1(x_2, x_43, x_53, x_45, x_12, x_3, x_52);
 lean_dec(x_45);
+lean_dec(x_2);
 if (lean_obj_tag(x_54) == 0)
 {
 lean_object* x_55; lean_object* x_56; lean_object* x_57; 
@@ -4055,6 +4031,7 @@ lean_object* x_107; lean_object* x_108;
 lean_dec(x_45);
 lean_dec(x_43);
 lean_dec(x_20);
+lean_dec(x_2);
 x_107 = lean_ctor_get(x_51, 0);
 lean_inc(x_107);
 x_108 = lean_ctor_get(x_51, 1);
@@ -4071,6 +4048,7 @@ lean_object* x_109; lean_object* x_110;
 lean_dec(x_45);
 lean_dec(x_43);
 lean_dec(x_20);
+lean_dec(x_2);
 x_109 = lean_ctor_get(x_48, 0);
 lean_inc(x_109);
 x_110 = lean_ctor_get(x_48, 1);
@@ -4088,6 +4066,7 @@ lean_object* x_188; lean_object* x_189;
 lean_dec(x_20);
 lean_dec(x_11);
 lean_dec(x_10);
+lean_dec(x_2);
 lean_dec(x_1);
 x_188 = lean_ctor_get(x_42, 0);
 lean_inc(x_188);
@@ -4161,6 +4140,7 @@ lean_dec(x_16);
 lean_dec(x_11);
 lean_dec(x_10);
 lean_dec(x_3);
+lean_dec(x_2);
 lean_dec(x_1);
 x_190 = !lean_is_exclusive(x_26);
 if (x_190 == 0)
@@ -4192,6 +4172,7 @@ lean_dec(x_16);
 lean_dec(x_11);
 lean_dec(x_10);
 lean_dec(x_3);
+lean_dec(x_2);
 lean_dec(x_1);
 x_194 = !lean_is_exclusive(x_24);
 if (x_194 == 0)
@@ -4221,11 +4202,10 @@ lean_dec(x_16);
 lean_dec(x_13);
 lean_dec(x_11);
 lean_dec(x_10);
+lean_dec(x_2);
 lean_dec(x_1);
 x_198 = l_Lean_Elab_Command_withDeclId___closed__3;
-x_199 = l_Lean_Elab_throwError___at_Lean_Elab_Command_elabCommand___spec__1(x_6, x_198, x_3, x_19);
-lean_dec(x_3);
-lean_dec(x_6);
+x_199 = l_Lean_Elab_Command_throwError___rarg(x_6, x_198, x_3, x_19);
 return x_199;
 }
 }
@@ -4239,6 +4219,7 @@ lean_dec(x_11);
 lean_dec(x_10);
 lean_dec(x_6);
 lean_dec(x_3);
+lean_dec(x_2);
 lean_dec(x_1);
 x_213 = !lean_is_exclusive(x_15);
 if (x_213 == 0)
@@ -4266,7 +4247,6 @@ _start:
 {
 lean_object* x_7; 
 x_7 = l_Array_iterateMAux___main___at_Lean_Elab_Command_elabAxiom___spec__5(x_1, x_2, x_3, x_4, x_5, x_6);
-lean_dec(x_5);
 lean_dec(x_2);
 lean_dec(x_1);
 return x_7;
@@ -4290,15 +4270,6 @@ lean_dec(x_1);
 return x_9;
 }
 }
-lean_object* l_Lean_Elab_Command_elabAxiom___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
-_start:
-{
-lean_object* x_5; 
-x_5 = l_Lean_Elab_Command_elabAxiom(x_1, x_2, x_3, x_4);
-lean_dec(x_2);
-return x_5;
-}
-}
 lean_object* l_Lean_Elab_Command_elabInductive___rarg(lean_object* x_1) {
 _start:
 {
@@ -4432,6 +4403,7 @@ _start:
 {
 lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; 
 x_4 = lean_ctor_get(x_1, 1);
+lean_inc(x_4);
 x_5 = l_Lean_stxInh;
 x_6 = lean_unsigned_to_nat(0u);
 x_7 = lean_array_get(x_5, x_4, x_6);
@@ -4449,6 +4421,7 @@ x_10 = lean_ctor_get(x_8, 0);
 x_11 = lean_ctor_get(x_8, 1);
 x_12 = lean_unsigned_to_nat(1u);
 x_13 = lean_array_get(x_5, x_4, x_12);
+lean_dec(x_4);
 lean_inc(x_13);
 x_14 = l_Lean_Syntax_getKind(x_13);
 x_15 = l_Lean_Parser_Command_abbrev___elambda__1___closed__2;
@@ -4506,14 +4479,14 @@ if (x_34 == 0)
 lean_object* x_35; lean_object* x_36; 
 lean_free_object(x_8);
 x_35 = l_Lean_Elab_Command_elabDeclaration___closed__4;
-x_36 = l_Lean_Elab_throwError___at_Lean_Elab_Command_elabCommand___spec__1(x_1, x_35, x_2, x_11);
-lean_dec(x_2);
+x_36 = l_Lean_Elab_Command_throwError___rarg(x_1, x_35, x_2, x_11);
 return x_36;
 }
 else
 {
 lean_object* x_37; 
 lean_dec(x_2);
+lean_dec(x_1);
 x_37 = lean_box(0);
 lean_ctor_set(x_8, 0, x_37);
 return x_8;
@@ -4524,6 +4497,7 @@ else
 lean_object* x_38; 
 lean_dec(x_14);
 lean_dec(x_2);
+lean_dec(x_1);
 x_38 = lean_box(0);
 lean_ctor_set(x_8, 0, x_38);
 return x_8;
@@ -4534,6 +4508,7 @@ else
 lean_object* x_39; 
 lean_dec(x_14);
 lean_dec(x_2);
+lean_dec(x_1);
 x_39 = lean_box(0);
 lean_ctor_set(x_8, 0, x_39);
 return x_8;
@@ -4544,6 +4519,7 @@ else
 lean_object* x_40; 
 lean_dec(x_14);
 lean_free_object(x_8);
+lean_dec(x_1);
 x_40 = l_Lean_Elab_Command_elabExample(x_10, x_13, x_2, x_11);
 return x_40;
 }
@@ -4553,8 +4529,8 @@ else
 lean_object* x_41; 
 lean_dec(x_14);
 lean_free_object(x_8);
+lean_dec(x_1);
 x_41 = l_Lean_Elab_Command_elabAxiom(x_10, x_13, x_2, x_11);
-lean_dec(x_13);
 return x_41;
 }
 }
@@ -4563,6 +4539,7 @@ else
 lean_object* x_42; 
 lean_dec(x_14);
 lean_free_object(x_8);
+lean_dec(x_1);
 x_42 = l_Lean_Elab_Command_elabInstance(x_10, x_13, x_2, x_11);
 return x_42;
 }
@@ -4572,6 +4549,7 @@ else
 lean_object* x_43; 
 lean_dec(x_14);
 lean_free_object(x_8);
+lean_dec(x_1);
 x_43 = l_Lean_Elab_Command_elabConstant(x_10, x_13, x_2, x_11);
 return x_43;
 }
@@ -4581,6 +4559,7 @@ else
 lean_object* x_44; 
 lean_dec(x_14);
 lean_free_object(x_8);
+lean_dec(x_1);
 x_44 = l_Lean_Elab_Command_elabTheorem(x_10, x_13, x_2, x_11);
 return x_44;
 }
@@ -4590,6 +4569,7 @@ else
 lean_object* x_45; 
 lean_dec(x_14);
 lean_free_object(x_8);
+lean_dec(x_1);
 x_45 = l_Lean_Elab_Command_elabDef(x_10, x_13, x_2, x_11);
 return x_45;
 }
@@ -4599,6 +4579,7 @@ else
 lean_object* x_46; 
 lean_dec(x_14);
 lean_free_object(x_8);
+lean_dec(x_1);
 x_46 = l_Lean_Elab_Command_elabAbbrev(x_10, x_13, x_2, x_11);
 return x_46;
 }
@@ -4613,6 +4594,7 @@ lean_inc(x_47);
 lean_dec(x_8);
 x_49 = lean_unsigned_to_nat(1u);
 x_50 = lean_array_get(x_5, x_4, x_49);
+lean_dec(x_4);
 lean_inc(x_50);
 x_51 = l_Lean_Syntax_getKind(x_50);
 x_52 = l_Lean_Parser_Command_abbrev___elambda__1___closed__2;
@@ -4669,14 +4651,14 @@ if (x_71 == 0)
 {
 lean_object* x_72; lean_object* x_73; 
 x_72 = l_Lean_Elab_Command_elabDeclaration___closed__4;
-x_73 = l_Lean_Elab_throwError___at_Lean_Elab_Command_elabCommand___spec__1(x_1, x_72, x_2, x_48);
-lean_dec(x_2);
+x_73 = l_Lean_Elab_Command_throwError___rarg(x_1, x_72, x_2, x_48);
 return x_73;
 }
 else
 {
 lean_object* x_74; lean_object* x_75; 
 lean_dec(x_2);
+lean_dec(x_1);
 x_74 = lean_box(0);
 x_75 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_75, 0, x_74);
@@ -4689,6 +4671,7 @@ else
 lean_object* x_76; lean_object* x_77; 
 lean_dec(x_51);
 lean_dec(x_2);
+lean_dec(x_1);
 x_76 = lean_box(0);
 x_77 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_77, 0, x_76);
@@ -4701,6 +4684,7 @@ else
 lean_object* x_78; lean_object* x_79; 
 lean_dec(x_51);
 lean_dec(x_2);
+lean_dec(x_1);
 x_78 = lean_box(0);
 x_79 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_79, 0, x_78);
@@ -4712,6 +4696,7 @@ else
 {
 lean_object* x_80; 
 lean_dec(x_51);
+lean_dec(x_1);
 x_80 = l_Lean_Elab_Command_elabExample(x_47, x_50, x_2, x_48);
 return x_80;
 }
@@ -4720,8 +4705,8 @@ else
 {
 lean_object* x_81; 
 lean_dec(x_51);
+lean_dec(x_1);
 x_81 = l_Lean_Elab_Command_elabAxiom(x_47, x_50, x_2, x_48);
-lean_dec(x_50);
 return x_81;
 }
 }
@@ -4729,6 +4714,7 @@ else
 {
 lean_object* x_82; 
 lean_dec(x_51);
+lean_dec(x_1);
 x_82 = l_Lean_Elab_Command_elabInstance(x_47, x_50, x_2, x_48);
 return x_82;
 }
@@ -4737,6 +4723,7 @@ else
 {
 lean_object* x_83; 
 lean_dec(x_51);
+lean_dec(x_1);
 x_83 = l_Lean_Elab_Command_elabConstant(x_47, x_50, x_2, x_48);
 return x_83;
 }
@@ -4745,6 +4732,7 @@ else
 {
 lean_object* x_84; 
 lean_dec(x_51);
+lean_dec(x_1);
 x_84 = l_Lean_Elab_Command_elabTheorem(x_47, x_50, x_2, x_48);
 return x_84;
 }
@@ -4753,6 +4741,7 @@ else
 {
 lean_object* x_85; 
 lean_dec(x_51);
+lean_dec(x_1);
 x_85 = l_Lean_Elab_Command_elabDef(x_47, x_50, x_2, x_48);
 return x_85;
 }
@@ -4761,6 +4750,7 @@ else
 {
 lean_object* x_86; 
 lean_dec(x_51);
+lean_dec(x_1);
 x_86 = l_Lean_Elab_Command_elabAbbrev(x_47, x_50, x_2, x_48);
 return x_86;
 }
@@ -4769,7 +4759,9 @@ return x_86;
 else
 {
 uint8_t x_87; 
+lean_dec(x_4);
 lean_dec(x_2);
+lean_dec(x_1);
 x_87 = !lean_is_exclusive(x_8);
 if (x_87 == 0)
 {
@@ -4791,15 +4783,6 @@ return x_90;
 }
 }
 }
-lean_object* l_Lean_Elab_Command_elabDeclaration___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
-{
-lean_object* x_4; 
-x_4 = l_Lean_Elab_Command_elabDeclaration(x_1, x_2, x_3);
-lean_dec(x_1);
-return x_4;
-}
-}
 lean_object* _init_l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclaration___closed__1() {
 _start:
 {
@@ -4822,7 +4805,7 @@ lean_object* _init_l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclaration__
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Command_elabDeclaration___boxed), 3, 0);
+x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Command_elabDeclaration), 3, 0);
 return x_1;
 }
 }

stage0/stdlib/Init/Lean/MetavarContext.c

@@ -46,6 +46,7 @@ lean_object* l_Lean_MetavarContext_instantiateMVars(lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_findAux___main___at_Lean_MetavarContext_findLevelDepth_x3f___spec__2___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_find_x3f___at_Lean_MetavarContext_findLevelDepth_x3f___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_MetavarContext_LevelMVarToParam_mkParamName___main___boxed(lean_object*);
+lean_object* l_Array_eraseIdx___rarg(lean_object*, lean_object*);
 lean_object* lean_array_uget(lean_object*, size_t);
 lean_object* l_Lean_MetavarContext_MkBinding_Lean_MonadHashMapCacheAdapter___lambda__2(lean_object*, lean_object*);
 extern lean_object* l_List_repr___rarg___closed__1;
@@ -171,6 +172,7 @@ lean_object* l_Lean_MetavarContext_hasAssignableMVar___main(lean_object*, lean_o
 uint8_t l_PersistentArray_anyMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__11(lean_object*, lean_object*);
 lean_object* l_PersistentArray_anyMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__11___boxed(lean_object*, lean_object*);
 uint8_t l_PersistentArray_anyMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__17(lean_object*, lean_object*);
+lean_object* l_Array_findIdxAux___main___at_Lean_LocalInstances_erase___spec__1(lean_object*, lean_object*, lean_object*);
 uint8_t l_Array_anyRangeMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__37(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_getAppNumArgsAux___main(lean_object*, lean_object*);
 uint8_t lean_metavar_ctx_is_expr_assigned(lean_object*, lean_object*);
@@ -285,6 +287,7 @@ lean_object* l_Array_indexOfAux___main___at_Lean_MetavarContext_eraseDelayed___s
 lean_object* l_Lean_MetavarContext_isWellFormed___main(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__43___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_PersistentHashMap_containsAux___main___at_Lean_MetavarContext_isExprAssigned___spec__2(lean_object*, size_t, lean_object*);
+lean_object* l_Lean_LocalInstances_erase(lean_object*, lean_object*);
 lean_object* l_PersistentArray_anyM___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__28___boxed(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_MetavarContext_16__abstractRangeAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentArray_anyM___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__16___boxed(lean_object*, lean_object*);
@@ -461,6 +464,7 @@ lean_object* l_Array_umapMAux___main___at___private_Init_Lean_MetavarContext_21_
 lean_object* l_Array_anyRangeMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_find_x3f___at_Lean_MetavarContext_getLevelAssignment_x3f___spec__1(lean_object*, lean_object*);
 lean_object* lean_mk_array(lean_object*, lean_object*);
+lean_object* l_Lean_LocalInstances_erase___boxed(lean_object*, lean_object*);
 lean_object* l_PersistentArray_anyMAux___main___at___private_Init_Lean_MetavarContext_20__anyDependsOn___spec__3___boxed(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_MetavarContext_8__dep___main___lambda__1(lean_object*, lean_object*);
 lean_object* l_Array_umapMAux___main___at___private_Init_Lean_MetavarContext_21__elimMVarDepsApp___main___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -470,6 +474,7 @@ lean_object* l_Lean_MetavarContext_MkBinding_Exception_toString___closed__1;
 lean_object* l___private_Init_Lean_MetavarContext_9__getLocalDeclWithSmallestIdx(lean_object*, lean_object*);
 uint8_t l_List_foldr___main___at_Lean_MetavarContext_hasAssignedMVar___main___spec__1(lean_object*, uint8_t, lean_object*);
 lean_object* l_PersistentHashMap_contains___at_Lean_MetavarContext_isDelayedAssigned___spec__1___boxed(lean_object*, lean_object*);
+lean_object* l_Array_findIdxAux___main___at_Lean_LocalInstances_erase___spec__1___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__44(lean_object*);
 lean_object* l___private_Init_Lean_MetavarContext_7__visit(lean_object*, lean_object*, lean_object*);
 uint8_t l_Array_anyRangeMAux___main___at___private_Init_Lean_MetavarContext_10__collectDeps___spec__32(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -606,6 +611,91 @@ x_1 = l_Lean_LocalInstance_hasBeq___closed__1;
 return x_1;
 }
 }
+lean_object* l_Array_findIdxAux___main___at_Lean_LocalInstances_erase___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; uint8_t x_5; 
+x_4 = lean_array_get_size(x_2);
+x_5 = lean_nat_dec_lt(x_3, x_4);
+lean_dec(x_4);
+if (x_5 == 0)
+{
+lean_object* x_6; 
+lean_dec(x_3);
+x_6 = lean_box(0);
+return x_6;
+}
+else
+{
+lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; 
+x_7 = lean_array_fget(x_2, x_3);
+x_8 = lean_ctor_get(x_7, 1);
+lean_inc(x_8);
+lean_dec(x_7);
+x_9 = l_Lean_Expr_fvarId_x21(x_8);
+lean_dec(x_8);
+x_10 = lean_name_eq(x_9, x_1);
+lean_dec(x_9);
+if (x_10 == 0)
+{
+lean_object* x_11; lean_object* x_12; 
+x_11 = lean_unsigned_to_nat(1u);
+x_12 = lean_nat_add(x_3, x_11);
+lean_dec(x_3);
+x_3 = x_12;
+goto _start;
+}
+else
+{
+lean_object* x_14; 
+x_14 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_14, 0, x_3);
+return x_14;
+}
+}
+}
+}
+lean_object* l_Lean_LocalInstances_erase(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; lean_object* x_4; 
+x_3 = lean_unsigned_to_nat(0u);
+x_4 = l_Array_findIdxAux___main___at_Lean_LocalInstances_erase___spec__1(x_2, x_1, x_3);
+if (lean_obj_tag(x_4) == 0)
+{
+return x_1;
+}
+else
+{
+lean_object* x_5; lean_object* x_6; 
+x_5 = lean_ctor_get(x_4, 0);
+lean_inc(x_5);
+lean_dec(x_4);
+x_6 = l_Array_eraseIdx___rarg(x_1, x_5);
+lean_dec(x_5);
+return x_6;
+}
+}
+}
+lean_object* l_Array_findIdxAux___main___at_Lean_LocalInstances_erase___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Array_findIdxAux___main___at_Lean_LocalInstances_erase___spec__1(x_1, x_2, x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_4;
+}
+}
+lean_object* l_Lean_LocalInstances_erase___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Lean_LocalInstances_erase(x_1, x_2);
+lean_dec(x_2);
+return x_3;
+}
+}
 uint8_t l_Lean_MetavarKind_isSyntheticOpaque(uint8_t x_1) {
 _start:
 {
@@ -2014,7 +2104,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l_Lean_MetavarContext_getDecl___closed__1;
-x_2 = lean_unsigned_to_nat(319u);
+x_2 = lean_unsigned_to_nat(325u);
 x_3 = lean_unsigned_to_nat(15u);
 x_4 = l_Lean_MetavarContext_getDecl___closed__2;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@@ -2244,7 +2334,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l_Lean_MetavarContext_getDecl___closed__1;
-x_2 = lean_unsigned_to_nat(327u);
+x_2 = lean_unsigned_to_nat(333u);
 x_3 = lean_unsigned_to_nat(12u);
 x_4 = l_Lean_MetavarContext_getDecl___closed__2;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@@ -5639,7 +5729,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l_Lean_MetavarContext_getDecl___closed__1;
-x_2 = lean_unsigned_to_nat(375u);
+x_2 = lean_unsigned_to_nat(381u);
 x_3 = lean_unsigned_to_nat(12u);
 x_4 = l_Lean_MetavarContext_isLevelAssignable___closed__1;
 x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);