chore: update stage0

2020-10-13 17:22:17 -07:00 · 2020-10-13 17:22:17 -07:00 · 725056cb87
commit 725056cb87
parent 1f09fc2c77
32 changed files with 24880 additions and 12519 deletions
--- a/stage0/src/Init/LeanInit.lean
+++ b/stage0/src/Init/LeanInit.lean
@ -248,6 +248,10 @@ match stx with
 | Syntax.node _ args => args.get! i
 | _                  => Syntax.missing -- panic! "Syntax.getArg: not a node"

+-- Add `stx[i]` as sugar for `stx.getArg i`
+@[inline] def getOp (self : Syntax) (idx : Nat) : Syntax :=
+self.getArg idx
+
 def getArgs (stx : Syntax) : Array Syntax :=
 match stx with
 | Syntax.node _ args => args
--- a/stage0/src/Lean/Elab/Attributes.lean
+++ b/stage0/src/Lean/Elab/Attributes.lean
@ -6,9 +6,8 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 import Lean.Parser.Basic
 import Lean.Attributes
 import Lean.MonadEnv
-
-namespace Lean
-namespace Elab
+new_frontend
+namespace Lean.Elab

 structure Attribute :=
 (name : Name) (args : Syntax := Syntax.missing)
@ -20,29 +19,27 @@ instance Attribute.inhabited : Inhabited Attribute := ⟨{ name := arbitrary _ }

 def elabAttr {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (stx : Syntax) : m Attribute := do
 -- rawIdent >> many attrArg
-let nameStx := stx.getArg 0;
-attrName ← match nameStx.isIdOrAtom? with
+let nameStx := stx[0]
+let attrName ← match nameStx.isIdOrAtom? with
  | none     => withRef nameStx $ throwError "identifier expected"
-  | some str => pure $ mkNameSimple str;
-env ← getEnv;
-unless (isAttribute env attrName) $
-  throwError ("unknown attribute [" ++ attrName ++ "]");
-let args := stx.getArg 1;
+  | some str => pure $ mkNameSimple str
+unless isAttribute (← getEnv) attrName do
+  throwError! "unknown attribute [{attrName}]"
+let args := stx[1]
 -- the old frontend passes Syntax.missing for empty args, for reasons
-let args := if args.getNumArgs == 0 then Syntax.missing else args;
+if args.getNumArgs == 0 then
+  args := Syntax.missing
 pure { name := attrName, args := args }

 -- sepBy1 attrInstance ", "
-def elabAttrs {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (stx : Syntax) : m (Array Attribute) :=
-stx.foldSepArgsM
-  (fun stx attrs => do
-    attr ← elabAttr stx;
-    pure $ attrs.push attr)
-  #[]
+def elabAttrs {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (stx : Syntax) : m (Array Attribute) := do
+let attrs := #[]
+for attr in stx.getSepArgs do
+  attrs := attrs.push (← elabAttr attr)
+return attrs

 -- parser! "@[" >> sepBy1 attrInstance ", " >> "]"
 def elabDeclAttrs {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (stx : Syntax) : m (Array Attribute) :=
-elabAttrs (stx.getArg 1)
+elabAttrs stx[1]

-end Elab
-end Lean
+end Lean.Elab
--- a/stage0/src/Lean/Elab/DeclUtil.lean
+++ b/stage0/src/Lean/Elab/DeclUtil.lean
@ -4,28 +4,27 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 import Lean.Meta.ExprDefEq
-
-namespace Lean
-namespace Meta
+new_frontend
+namespace Lean.Meta

 def forallTelescopeCompatibleAux {α} (k : Array Expr → Expr → Expr → MetaM α) : Nat → Expr → Expr → Array Expr → MetaM α
 | 0, type₁, type₂, xs   => k xs type₁ type₂
 | i+1, type₁, type₂, xs => do
-  type₁ ← whnf type₁;
-  type₂ ← whnf type₂;
+  let type₁ ← whnf type₁
+  let type₂ ← whnf type₂
  match type₁, type₂ with
-  | Expr.forallE n₁ d₁ b₁ c₁, Expr.forallE n₂ d₂ b₂ c₂ => do
-    unless (n₁ == n₂) $
-      throwError ("parameter name mismatch '" ++ n₁ ++ "', expected '" ++ n₂ ++ "'");
-    unlessM (isDefEq d₁ d₂) $
-      throwError ("type mismatch at parameter '" ++ n₁ ++ "'" ++ indentExpr d₁  ++ Format.line ++ "expected type" ++ indentExpr d₂);
-    unless (c₁.binderInfo == c₂.binderInfo) $
-      throwError ("binder annotation mismatch at parameter '" ++ n₁ ++ "'");
+  | Expr.forallE n₁ d₁ b₁ c₁, Expr.forallE n₂ d₂ b₂ c₂ =>
+    unless n₁ == n₂ do
+      throwError! "parameter name mismatch '{n₁}', expected '{n₂}'"
+    unless (← isDefEq d₁ d₂) do
+      throwError! "type mismatch at parameter '{n₁}'{indentExpr d₁}\nexpected type{indentExpr d₂}"
+    unless c₁.binderInfo == c₂.binderInfo do
+      throwError! "binder annotation mismatch at parameter '{n₁}'"
    withLocalDecl n₁ c₁.binderInfo d₁ fun x =>
-      let type₁ := b₁.instantiate1 x;
-      let type₂ := b₂.instantiate1 x;
-      forallTelescopeCompatibleAux i type₁ type₂ (xs.push x)
-  | _, _ => throwError ("unexpected number of parameters")
+      let type₁ := b₁.instantiate1 x
+      let type₂ := b₂.instantiate1 x
+      forallTelescopeCompatibleAux k i type₁ type₂ (xs.push x)
+  | _, _ => throwError "unexpected number of parameters"

 /-- Given two forall-expressions `type₁` and `type₂`, ensure the first `numParams` parameters are compatible, and
    then execute `k` with the parameters and remaining types. -/
@ -38,19 +37,19 @@ namespace Elab

 def expandOptDeclSig (stx : Syntax) : Syntax × Option Syntax :=
 -- many Term.bracketedBinder >> Term.optType
-let binders := stx.getArg 0;
-let optType := stx.getArg 1; -- optional (parser! " : " >> termParser)
+let binders := stx[0]
+let optType := stx[1] -- optional (parser! " : " >> termParser)
 if optType.isNone then
  (binders, none)
 else
-  let typeSpec := optType.getArg 0;
-  (binders, some $ typeSpec.getArg 1)
+  let typeSpec := optType[0]
+  (binders, some typeSpec[1])

 def expandDeclSig (stx : Syntax) : Syntax × Syntax :=
 -- many Term.bracketedBinder >> Term.typeSpec
-let binders := stx.getArg 0;
-let typeSpec := stx.getArg 1;
-(binders, typeSpec.getArg 1)
+let binders  := stx[0]
+let typeSpec := stx[1]
+(binders, typeSpec[1])

 def mkFreshInstanceName (env : Environment) (nextIdx : Nat) : Name :=
 (env.mainModule ++ `_instance).appendIndexAfter nextIdx
@ -73,11 +72,11 @@ match name with
  Remark: `explicitParams` are in reverse declaration order. That is, the head is the last declared parameter. -/
 def sortDeclLevelParams (scopeParams : List Name) (allUserParams : List Name) (usedParams : Array Name) : Except String (List Name) :=
 match allUserParams.find? $ fun u => !usedParams.contains u && !scopeParams.elem u with
-| some u => throw ("unused universe parameter '" ++ toString u ++ "'")
+| some u => throw s!"unused universe parameter '{u}'"
 | none   =>
-  let result := allUserParams.foldl (fun result levelName => if usedParams.elem levelName then levelName :: result else result) [];
-  let remaining := usedParams.filter (fun levelParam => !allUserParams.elem levelParam);
-  let remaining := remaining.qsort Name.lt;
+  let result := allUserParams.foldl (fun result levelName => if usedParams.elem levelName then levelName :: result else result) []
+  let remaining := usedParams.filter (fun levelParam => !allUserParams.elem levelParam)
+  let remaining := remaining.qsort Name.lt
  pure $ result ++ remaining.toList

 end Elab
--- a/stage0/src/Lean/Elab/Declaration.lean
+++ b/stage0/src/Lean/Elab/Declaration.lean
@ -9,21 +9,19 @@ import Lean.Elab.DefView
 import Lean.Elab.Inductive
 import Lean.Elab.Structure
 import Lean.Elab.MutualDef
-
-namespace Lean
-namespace Elab
-namespace Command
+new_frontend
+namespace Lean.Elab.Command

 open Meta

 /- Auxiliary function for `expandDeclNamespace?` -/
 def expandDeclIdNamespace? (declId : Syntax) : Option (Name × Syntax) :=
-let (id, optUnivDeclStx) := expandDeclIdCore declId;
-let scpView := extractMacroScopes id;
+let (id, optUnivDeclStx) := expandDeclIdCore declId
+let scpView := extractMacroScopes id
 match scpView.name with
 | Name.str Name.anonymous s _ => none
 | Name.str pre s _            =>
-  let nameNew := { scpView with name := mkNameSimple s }.review;
+  let nameNew := { scpView with name := mkNameSimple s }.review
  if declId.isIdent then
    some (pre, mkIdentFrom declId nameNew)
  else
@ -34,8 +32,8 @@ match scpView.name with
 def expandDeclNamespace? (stx : Syntax) : Option (Name × Syntax) :=
 if !stx.isOfKind `Lean.Parser.Command.declaration then none
 else
-  let decl := stx.getArg 1;
-  let k := decl.getKind;
+  let decl := stx[1]
+  let k := decl.getKind
  if k == `Lean.Parser.Command.abbrev ||
     k == `Lean.Parser.Command.def ||
     k == `Lean.Parser.Command.theorem ||
@ -43,17 +41,17 @@ else
     k == `Lean.Parser.Command.axiom ||
     k == `Lean.Parser.Command.inductive ||
     k == `Lean.Parser.Command.structure then
-    match expandDeclIdNamespace? (decl.getArg 1) with
+    match expandDeclIdNamespace? decl[1] with
    | some (ns, declId) => some (ns, stx.setArg 1 (decl.setArg 1 declId))
    | none              => none
  else if k == `Lean.Parser.Command.instance then
-    let optDeclId := decl.getArg 1;
+    let optDeclId := decl[1]
    if optDeclId.isNone then none
-    else match expandDeclIdNamespace? (optDeclId.getArg 0) with
+    else match expandDeclIdNamespace? optDeclId[0] with
      | some (ns, declId) => some (ns, stx.setArg 1 (decl.setArg 1 (optDeclId.setArg 0 declId)))
      | none              => none
  else if k == `Lean.Parser.Command.classInductive then
-    match expandDeclIdNamespace? (decl.getArg 2) with
+    match expandDeclIdNamespace? decl[2] with
    | some (ns, declId) => some (ns, stx.setArg 1 (decl.setArg 2 declId))
    | none              => none
  else
@ -61,31 +59,31 @@ else

 def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
 -- parser! "axiom " >> declId >> declSig
-let declId             := stx.getArg 1;
-let (binders, typeStx) := expandDeclSig (stx.getArg 2);
-scopeLevelNames ← getLevelNames;
-⟨name, declName, allUserLevelNames⟩ ← expandDeclId declId modifiers;
-runTermElabM declName $ fun vars => Term.withLevelNames allUserLevelNames $ Term.elabBinders binders.getArgs fun xs => do
-  Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.beforeElaboration;
-  type ← Term.elabType typeStx;
-  Term.synthesizeSyntheticMVarsNoPostponing;
-  type ← instantiateMVars type;
-  type ← mkForallFVars xs type;
-  (type, _) ← mkForallUsedOnly vars type;
-  (type, _) ← Term.levelMVarToParam type;
-  let usedParams  := (collectLevelParams {} type).params;
+let declId             := stx[1]
+let (binders, typeStx) := expandDeclSig stx[2]
+let scopeLevelNames ← getLevelNames
+let ⟨name, declName, allUserLevelNames⟩ ← expandDeclId declId modifiers
+runTermElabM declName fun vars => Term.withLevelNames allUserLevelNames $ Term.elabBinders binders.getArgs fun xs => do
+  Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.beforeElaboration
+  let type ← Term.elabType typeStx
+  Term.synthesizeSyntheticMVarsNoPostponing
+  let type ← instantiateMVars type
+  let type ← mkForallFVars xs type
+  let (type, _) ← mkForallUsedOnly vars type
+  let (type, _) ← Term.levelMVarToParam type
+  let usedParams  := collectLevelParams {} type $.params
  match sortDeclLevelParams scopeLevelNames allUserLevelNames usedParams with
  | Except.error msg      => throwErrorAt stx msg
-  | Except.ok levelParams => do
+  | Except.ok levelParams =>
    let decl := Declaration.axiomDecl {
      name     := declName,
      lparams  := levelParams,
      type     := type,
      isUnsafe := modifiers.isUnsafe
-    };
-    Term.ensureNoUnassignedMVars decl;
-    addDecl decl;
-    Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterTypeChecking;
+    }
+    Term.ensureNoUnassignedMVars decl
+    addDecl decl
+    Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterTypeChecking
    Term.applyAttributesAt declName modifiers.attrs AttributeApplicationTime.afterCompilation

 /-
@ -95,25 +93,24 @@ parser! try ("class " >> "inductive ") >> declId >> optDeclSig >> many ctor
 Remark: numTokens == 1 for regular `inductive` and 2 for `class inductive`.
 -/
 private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) (numTokens := 1) : CommandElabM InductiveView := do
-checkValidInductiveModifier modifiers;
-let (binders, type?) := expandOptDeclSig (decl.getArg (numTokens + 1));
-let declId           := decl.getArg numTokens;
-⟨name, declName, levelNames⟩ ← expandDeclId declId modifiers;
-ctors      ← (decl.getArg (numTokens + 2)).getArgs.mapM fun ctor => withRef ctor do {
+checkValidInductiveModifier modifiers
+let (binders, type?) := expandOptDeclSig decl[numTokens + 1]
+let declId           := decl[numTokens]
+let ⟨name, declName, levelNames⟩ ← expandDeclId declId modifiers
+let ctors      ← decl[numTokens + 2].getArgs.mapM fun ctor => withRef ctor do
  -- def ctor := parser! " | " >> declModifiers >> ident >> optional inferMod >> optDeclSig
-  ctorModifiers ← elabModifiers (ctor.getArg 1);
-  when (ctorModifiers.isPrivate && modifiers.isPrivate) $
-    throwError "invalid 'private' constructor in a 'private' inductive datatype";
-  when (ctorModifiers.isProtected && modifiers.isPrivate) $
-    throwError "invalid 'protected' constructor in a 'private' inductive datatype";
-  checkValidCtorModifier ctorModifiers;
-  let ctorName := ctor.getIdAt 2;
-  let ctorName := declName ++ ctorName;
-  ctorName ← withRef (ctor.getArg 2) $ applyVisibility ctorModifiers.visibility ctorName;
-  let inferMod := !(ctor.getArg 3).isNone;
-  let (binders, type?) := expandOptDeclSig (ctor.getArg 4);
+  let ctorModifiers ← elabModifiers ctor[1]
+  if ctorModifiers.isPrivate && modifiers.isPrivate then
+    throwError "invalid 'private' constructor in a 'private' inductive datatype"
+  if ctorModifiers.isProtected && modifiers.isPrivate then
+    throwError "invalid 'protected' constructor in a 'private' inductive datatype"
+  checkValidCtorModifier ctorModifiers
+  let ctorName := ctor.getIdAt 2
+  let ctorName := declName ++ ctorName
+  let ctorName ← withRef ctor[2] $ applyVisibility ctorModifiers.visibility ctorName
+  let inferMod := !ctor[3].isNone
+  let (binders, type?) := expandOptDeclSig ctor[4]
  pure { ref := ctor, modifiers := ctorModifiers, declName := ctorName, inferMod := inferMod, binders := binders, type? := type? : CtorView }
-};
 pure {
  ref           := decl,
  modifiers     := modifiers,
@ -129,60 +126,59 @@ private def classInductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) :
 inductiveSyntaxToView modifiers decl 2

 def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
-v ← inductiveSyntaxToView modifiers stx;
+let v ← inductiveSyntaxToView modifiers stx
 elabInductiveViews #[v]

 def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
-let modifiers := modifiers.addAttribute { name := `class };
-v ← classInductiveSyntaxToView modifiers stx;
+let modifiers := modifiers.addAttribute { name := `class }
+let v ← classInductiveSyntaxToView modifiers stx
 elabInductiveViews #[v]

@[builtinCommandElab declaration]
 def elabDeclaration : CommandElab :=
 fun stx => match expandDeclNamespace? stx with
 | some (ns, newStx) => do
-  let ns := mkIdentFrom stx ns;
-  newStx ← `(namespace $ns:ident $newStx end $ns:ident);
+  let ns := mkIdentFrom stx ns
+  let newStx ← `(namespace $ns:ident $newStx end $ns:ident)
  withMacroExpansion stx newStx $ elabCommand newStx
 | none => do
-  modifiers ← elabModifiers (stx.getArg 0);
-  let decl     := stx.getArg 1;
-  let declKind := decl.getKind;
-  if declKind == `Lean.Parser.Command.axiom then
+  let modifiers ← elabModifiers stx[0]
+  let decl     := stx[1]
+  let declKind := decl.getKind
+  if declKind == `Lean.Parser.Command.«axiom» then
    elabAxiom modifiers decl
-  else if declKind == `Lean.Parser.Command.inductive then
+  else if declKind == `Lean.Parser.Command.«inductive» then
    elabInductive modifiers decl
  else if declKind == `Lean.Parser.Command.classInductive then
    elabClassInductive modifiers decl
-  else if declKind == `Lean.Parser.Command.structure then
+  else if declKind == `Lean.Parser.Command.«structure» then
    elabStructure modifiers decl
-  else if isDefLike decl then do
+  else if isDefLike decl then
    elabMutualDef #[stx]
  else
    throwError "unexpected declaration"

 /- Return true if all elements of the mutual-block are inductive declarations. -/
 private def isMutualInductive (stx : Syntax) : Bool :=
-(stx.getArg 1).getArgs.all $ fun elem =>
-  let decl     := elem.getArg 1;
-  let declKind := decl.getKind;
+stx[1].getArgs.all fun elem =>
+  let decl     := elem[1]
+  let declKind := decl.getKind
  declKind == `Lean.Parser.Command.inductive

 private def elabMutualInductive (elems : Array Syntax) : CommandElabM Unit := do
-views ← elems.mapM $ fun stx => do {
-   modifiers ← elabModifiers (stx.getArg 0);
-   inductiveSyntaxToView modifiers (stx.getArg 1)
-};
+let views ← elems.mapM fun stx => do
+   let modifiers ← elabModifiers stx[0]
+   inductiveSyntaxToView modifiers stx[1]
 elabInductiveViews views

 /- Return true if all elements of the mutual-block are definitions/theorems/abbrevs. -/
 private def isMutualDef (stx : Syntax) : Bool :=
-(stx.getArg 1).getArgs.all $ fun elem =>
-  let decl := elem.getArg 1;
+stx[1].getArgs.all fun elem =>
+  let decl := elem[1]
  isDefLike decl

 private def isMutualPreambleCommand (stx : Syntax) : Bool :=
-let k := stx.getKind;
+let k := stx.getKind
 k == `Lean.Parser.Command.variable ||
 k == `Lean.Parser.Command.variables ||
 k == `Lean.Parser.Command.universe ||
@ -191,53 +187,48 @@ k == `Lean.Parser.Command.check ||
 k == `Lean.Parser.Command.set_option ||
 k == `Lean.Parser.Command.open

-private partial def splitMutualPreamble (elems : Array Syntax) : Nat → Option (Array Syntax × Array Syntax)
-| i =>
+private partial def splitMutualPreamble (elems : Array Syntax) : Option (Array Syntax × Array Syntax) :=
+let rec loop (i : Nat) : Option (Array Syntax × Array Syntax) :=
  if h : i < elems.size then
-    let elem := elems.get ⟨i, h⟩;
+    let elem := elems.get ⟨i, h⟩
    if isMutualPreambleCommand elem then
-      splitMutualPreamble (i+1)
+      loop (i+1)
    else if i == 0 then
      none -- `mutual` block does not contain any preamble commands
    else
-      some (elems.extract 0 i, elems.extract i elems.size)
+      some (elems[0:i], elems[i:elems.size])
  else
    none -- a `mutual` block containing only preamble commands is not a valid `mutual` block
+loop 0

@[builtinMacro Lean.Parser.Command.mutual] def expandMutualNamespace : Macro :=
 fun stx => do
-  let elems := (stx.getArg 1).getArgs;
-  (ns?, elems) ← elems.foldlM
-    (fun (acc : Option Name × Array Syntax) (elem : Syntax) =>
-      let (ns?, elems) := acc;
-      match ns?, expandDeclNamespace? elem with
-      | _, none                         => pure (ns?, elems.push elem)
-      | none, some (ns, elem)           => pure (some ns, elems.push elem)
-      | some nsCurr, some (nsNew, elem) =>
-        if nsCurr == nsNew then
-          pure (ns?, elems.push elem)
-        else
-          Macro.throwError elem
-            ("conflicting namespaces in mutual declaration, using namespace '" ++ toString nsNew ++ "', but used '" ++ toString nsCurr ++ "' in previous declaration"))
-    (none, #[]);
+  let ns?      := none
+  let elemsNew := #[]
+  for elem in stx[1].getArgs do
+    match ns?, expandDeclNamespace? elem with
+    | _, none                         => elemsNew := elemsNew.push elem
+    | none, some (ns, elem)           => ns? := some ns; elemsNew := elemsNew.push elem
+    | some nsCurr, some (nsNew, elem) =>
+      if nsCurr == nsNew then
+        elemsNew := elemsNew.push elem
+      else
+        Macro.throwError elem s!"conflicting namespaces in mutual declaration, using namespace '{nsNew}', but used '{nsCurr}' in previous declaration"
  match ns? with
  | some ns =>
-    let ns := mkIdentFrom stx ns;
-    let stxNew := stx.setArg 1 (mkNullNode elems);
+    let ns := mkIdentFrom stx ns
+    let stxNew := stx.setArg 1 (mkNullNode elemsNew)
    `(namespace $ns:ident $stxNew end $ns:ident)
  | none => Macro.throwUnsupported

@[builtinMacro Lean.Parser.Command.mutual] def expandMutualElement : Macro :=
 fun stx => do
-  let elems := (stx.getArg 1).getArgs;
-  (elemsNew, modified) ← elems.foldlM
-    (fun (acc : Array Syntax × Bool) elem => do
-       let (elemsNew, modified) := acc;
-       elem? ← expandMacro? elem;
-       match elem? with
-       | some elemNew => pure (elemsNew.push elemNew, true)
-       | none         => pure (elemsNew.push elem, modified))
-    (#[], false);
+  let elemsNew := #[]
+  let modified := false
+  for elem in stx[1].getArgs do
+    match (← expandMacro? elem) with
+    | some elemNew => elemsNew := elemsNew.push elemNew; modified := true
+    | none         => elemsNew := elemsNew.push elem
  if modified then
    pure $ stx.setArg 1 (mkNullNode elemsNew)
  else
@ -245,45 +236,44 @@ fun stx => do

@[builtinMacro Lean.Parser.Command.mutual] def expandMutualPreamble : Macro :=
 fun stx =>
-  match splitMutualPreamble (stx.getArg 1).getArgs 0 with
+  match splitMutualPreamble stx[1].getArgs with
  | none => Macro.throwUnsupported
  | some (preamble, rest) => do
-    secCmd    ← `(section);
-    let newMutual := stx.setArg 1 (mkNullNode rest);
-    endCmd    ← `(end);
+    let secCmd    ← `(section)
+    let newMutual := stx.setArg 1 (mkNullNode rest)
+    let endCmd    ← `(end)
    pure $ mkNullNode (#[secCmd] ++ preamble ++ #[newMutual] ++ #[endCmd])

@[builtinCommandElab «mutual»]
 def elabMutual : CommandElab :=
 fun stx => do
  if isMutualInductive stx then
-    elabMutualInductive (stx.getArg 1).getArgs
+    elabMutualInductive stx[1].getArgs
  else if isMutualDef stx then
-    elabMutualDef (stx.getArg 1).getArgs
+    elabMutualDef stx[1].getArgs
  else
    throwError "invalid mutual block"

 /- parser! optional "local " >> "attribute " >> "[" >> sepBy1 Term.attrInstance ", " >> "]" >> many1 ident -/
@[builtinCommandElab «attribute»] def elabAttr : CommandElab :=
 fun stx => do
-  let persistent := (stx.getArg 0).isNone;
-  attrs ← elabAttrs (stx.getArg 3);
-  let idents := (stx.getArg 5).getArgs;
-  idents.forM fun ident => withRef ident $ liftTermElabM none do
-    declName ← resolveGlobalConstNoOverload ident.getId;
+  let persistent := stx[0].isNone
+  let attrs ← elabAttrs stx[3]
+  let idents := stx[5].getArgs
+  for ident in idents do withRef ident $ liftTermElabM none do
+    let declName ← resolveGlobalConstNoOverload ident.getId
    Term.applyAttributes declName attrs persistent

@[builtinMacro Lean.Parser.Command.«initialize»] def expandInitialize : Macro :=
 fun stx =>
-  let optHeader := stx.getArg 1;
-  let doSeq     := stx.getArg 2;
+  let optHeader := stx[1]
+  let doSeq     := stx[2]
  if optHeader.isNone then
    `(@[init]def initFn : IO Unit := do $doSeq)
  else
-    let id   := optHeader.getArg 0;
-    let type := (optHeader.getArg 1).getArg 1;
-    `(def initFn : IO $type := do $doSeq @[init initFn]constant $id : $type)
+    let id   := optHeader[0]
+    let type := optHeader[1][1]
+    `(def initFn : IO $type := do $doSeq
+      @[init initFn]constant $id : $type)

-end Command
-end Elab
-end Lean
+end Lean.Elab.Command
--- a/stage0/src/Lean/Elab/Import.lean
+++ b/stage0/src/Lean/Elab/Import.lean
@ -4,47 +4,44 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 import Lean.Parser.Module
-
-namespace Lean
-namespace Elab
+new_frontend
+namespace Lean.Elab

 def headerToImports (header : Syntax) : List Import :=
-let header  := header.asNode;
-let imports := if (header.getArg 0).isNone then [{ module := `Init : Import }] else [];
-imports ++ (header.getArg 1).getArgs.toList.map (fun stx =>
+let imports := if header[0].isNone then [{ module := `Init : Import }] else []
+imports ++ header[1].getArgs.toList.map fun stx =>
  -- `stx` is of the form `(Module.import "import" "runtime"? id)
-  let runtime := !(stx.getArg 1).isNone;
-  let id      := stx.getIdAt 2;
-  { module := id, runtimeOnly := runtime })
+  let runtime := !stx[1].isNone
+  let id      := stx[2].getId
+  { module := id, runtimeOnly := runtime }

-def processHeader (header : Syntax) (messages : MessageLog) (inputCtx : Parser.InputContext) (trustLevel : UInt32 := 0) : IO (Environment × MessageLog) :=
-catch
-  (do env ← importModules (headerToImports header) trustLevel;
-      pure (env, messages))
-  (fun e => do
-     env ← mkEmptyEnvironment;
-     let spos := header.getPos.getD 0;
-     let pos  := inputCtx.fileMap.toPosition spos;
-     pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos }))
+def processHeader (header : Syntax) (messages : MessageLog) (inputCtx : Parser.InputContext) (trustLevel : UInt32 := 0) : IO (Environment × MessageLog) := do
+try
+  let env ← importModules (headerToImports header) trustLevel
+  pure (env, messages)
+catch e =>
+  let env ← mkEmptyEnvironment
+  let spos := header.getPos.getD 0
+  let pos  := inputCtx.fileMap.toPosition spos
+  pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos })

 def parseImports (input : String) (fileName : Option String := none) : IO (List Import × Position × MessageLog) := do
-env ← mkEmptyEnvironment;
-let fileName := fileName.getD "<input>";
-let inputCtx := Parser.mkInputContext input fileName;
+let env ← mkEmptyEnvironment
+let fileName := fileName.getD "<input>"
+let inputCtx := Parser.mkInputContext input fileName
 match Parser.parseHeader env inputCtx with
-| (header, parserState, messages) => do
+| (header, parserState, messages) =>
  pure (headerToImports header, inputCtx.fileMap.toPosition parserState.pos, messages)

@[export lean_parse_imports]
 def parseImportsExport (input : String) (fileName : Option String) : IO (List Import × Position × List Message) := do
-(imports, pos, log) ← parseImports input fileName;
+let (imports, pos, log) ← parseImports input fileName
 pure (imports, pos, log.toList)

@[export lean_print_deps]
-def printDeps (deps : List Import) : IO Unit :=
-deps.forM $ fun dep => do
-  fname ← findOLean dep.module;
+def printDeps (deps : List Import) : IO Unit := do
+for dep in deps do
+  let fname ← findOLean dep.module;
  IO.println fname

-end Elab
-end Lean
+end Lean.Elab
--- a/stage0/src/Lean/Elab/LetRec.lean
+++ b/stage0/src/Lean/Elab/LetRec.lean
@ -7,11 +7,8 @@ import Lean.Elab.Attributes
 import Lean.Elab.Binders
 import Lean.Elab.DeclModifiers
 import Lean.Elab.SyntheticMVars
-
-namespace Lean
-namespace Elab
-namespace Term
-
+new_frontend
+namespace Lean.Elab.Term
 open Meta

 structure LetRecDeclView :=
@ -30,32 +27,31 @@ structure LetRecView :=

 /-  group ("let " >> nonReservedSymbol "rec ") >> sepBy1 (group (optional «attributes» >> letDecl)) ", " >> "; " >> termParser -/
 private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
-decls ← (letRec.getArg 1).getSepArgs.mapM fun attrDeclStx => do {
-  let attrOptStx := attrDeclStx.getArg 0;
-  attrs ← if attrOptStx.isNone then pure #[] else elabDeclAttrs (attrOptStx.getArg 0);
-  let decl := (attrDeclStx.getArg 1).getArg 0;
+let decls ← letRec[1].getSepArgs.mapM fun (attrDeclStx : Syntax) => do
+  let attrOptStx := attrDeclStx[0]
+  let attrs ← if attrOptStx.isNone then pure #[] else elabDeclAttrs attrOptStx[0]
+  let decl := attrDeclStx[1][0]
  if decl.isOfKind `Lean.Parser.Term.letPatDecl then
    throwErrorAt decl "patterns are not allowed in 'let rec' expressions"
-  else if decl.isOfKind `Lean.Parser.Term.letIdDecl || decl.isOfKind `Lean.Parser.Term.letEqnsDecl then do
-    let shortDeclName := decl.getIdAt 0;
-    currDeclName? ← getDeclName?;
-    let declName := currDeclName?.getD Name.anonymous ++ shortDeclName;
-    checkNotAlreadyDeclared declName;
-    applyAttributesAt declName attrs AttributeApplicationTime.beforeElaboration;
-    let binders := (decl.getArg 1).getArgs;
-    let typeStx := expandOptType decl (decl.getArg 2);
-    (type, numParams) ← elabBinders binders fun xs => do {
-        type ← elabType typeStx;
-        registerCustomErrorIfMVar type typeStx "failed to infer 'let rec' declaration type";
-        type ← mkForallFVars xs type;
+  else if decl.isOfKind `Lean.Parser.Term.letIdDecl || decl.isOfKind `Lean.Parser.Term.letEqnsDecl then
+    let shortDeclName := decl[0].getId
+    let currDeclName? ← getDeclName?
+    let declName := currDeclName?.getD Name.anonymous ++ shortDeclName
+    checkNotAlreadyDeclared declName
+    applyAttributesAt declName attrs AttributeApplicationTime.beforeElaboration
+    let binders := decl[1].getArgs
+    let typeStx := expandOptType decl decl[2]
+    let (type, numParams) ← elabBinders binders fun xs => do
+        let type ← elabType typeStx
+        registerCustomErrorIfMVar type typeStx "failed to infer 'let rec' declaration type"
+        let type ← mkForallFVars xs type
        pure (type, xs.size)
-    };
-    mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque;
-    valStx ←
+    let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
+    let valStx ←
      if decl.isOfKind `Lean.Parser.Term.letIdDecl then
-        pure $ decl.getArg 4
+        pure decl[4]
      else
-        liftMacroM $ expandMatchAltsIntoMatch decl (decl.getArg 3);
+        liftMacroM $ expandMatchAltsIntoMatch decl decl[3]
    pure {
      ref           := decl,
      attrs         := attrs,
@ -68,58 +64,55 @@ decls ← (letRec.getArg 1).getSepArgs.mapM fun attrDeclStx => do {
      : LetRecDeclView }
  else
    throwUnsupportedSyntax
-};
 pure {
  decls := decls,
-  body  := letRec.getArg 3
+  body  := letRec[3]
 }

-private partial def withAuxLocalDeclsAux {α} (views : Array LetRecDeclView) (k : Array Expr → TermElabM α) : Nat → Array Expr → TermElabM α
-| i, fvars =>
+private partial def withAuxLocalDecls {α} (views : Array LetRecDeclView) (k : Array Expr → TermElabM α) : TermElabM α :=
+let rec loop (i : Nat) (fvars : Array Expr) : TermElabM α :=
  if h : i < views.size then
-    let view := views.get ⟨i, h⟩;
-    withLetDecl view.shortDeclName view.type view.mvar fun fvar => withAuxLocalDeclsAux (i+1) (fvars.push fvar)
+    let view := views.get ⟨i, h⟩
+    withLetDecl view.shortDeclName view.type view.mvar fun fvar => loop (i+1) (fvars.push fvar)
  else
    k fvars
-
-private def withAuxLocalDecls {α} (views : Array LetRecDeclView) (k : Array Expr → TermElabM α) : TermElabM α :=
-withAuxLocalDeclsAux views k 0 #[]
+loop 0 #[]

 private def elabLetRecDeclValues (view : LetRecView) : TermElabM (Array Expr) :=
 view.decls.mapM fun view => do
  forallBoundedTelescope view.type view.numParams fun xs type =>
     withDeclName view.declName do
-       value ← elabTermEnsuringType view.valStx type;
+       let value ← elabTermEnsuringType view.valStx type
       mkLambdaFVars xs value

 private def abortIfContainsSyntheticSorry (e : Expr) : TermElabM Unit := do
-e ← instantiateMVars e;
-when e.hasSyntheticSorry $ throwAbort
+let e ← instantiateMVars e
+if e.hasSyntheticSorry then throwAbort

 private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array Expr) (values : Array Expr) : TermElabM Unit := do
-lctx ← getLCtx;
-localInsts ← getLocalInstances;
+let lctx ← getLCtx
+let localInsts ← getLocalInstances
 let toLift := views.mapIdx fun i view => {
  ref            := view.ref,
-  fvarId         := (fvars.get! i).fvarId!,
+  fvarId         := fvars[i].fvarId!,
  attrs          := view.attrs,
  shortDeclName  := view.shortDeclName,
  declName       := view.declName,
  lctx           := lctx,
  localInstances := localInsts,
  type           := view.type,
-  val            := values.get! i,
+  val            := values[i],
  mvarId         := view.mvar.mvarId!
-  : LetRecToLift };
+  : LetRecToLift }
 modify fun s => { s with letRecsToLift := toLift.toList ++ s.letRecsToLift }

@[builtinTermElab «letrec»] def elabLetRec : TermElab :=
 fun stx expectedType? => do
-  view ← mkLetRecDeclView stx;
+  let view ← mkLetRecDeclView stx
  withAuxLocalDecls view.decls fun fvars => do
-    values ← elabLetRecDeclValues view;
-    body ← elabTermEnsuringType view.body expectedType?;
-    registerLetRecsToLift view.decls fvars values;
+    let values ← elabLetRecDeclValues view
+    let body ← elabTermEnsuringType view.body expectedType?
+    registerLetRecsToLift view.decls fvars values
    mkLetFVars fvars body

 end Term
--- a/stage0/src/Lean/Elab/Print.lean
+++ b/stage0/src/Lean/Elab/Print.lean
@ -73,7 +73,7 @@ cs.forM printIdCore
 fun stx =>
  let numArgs := stx.getNumArgs
  if numArgs == 2 then
-    let arg := stx.getArg 1
+    let arg := stx[1]
    if arg.isIdent then
      printId arg.getId
    else match arg.isStrLit? with
@ -120,7 +120,7 @@ else

@[builtinCommandElab «printAxioms»] def elabPrintAxioms : CommandElab :=
 fun stx => do
-  let id := (stx.getArg 2).getId
+  let id := stx[2].getId
  let cs ← resolveGlobalConst id
  cs.forM printAxiomsOf

--- a/stage0/src/Lean/Elab/Syntax.lean
+++ b/stage0/src/Lean/Elab/Syntax.lean
@ -5,13 +5,8 @@ Authors: Leonardo de Moura
 -/
 import Lean.Elab.Command
 import Lean.Elab.Quotation
-
-namespace Lean
-namespace Elab
-open MonadResolveName (getCurrNamespace getOpenDecls) -- HACK for old frontend
-
-namespace Term
-
+new_frontend
+namespace Lean.Elab.Term
 /-
 Expand `optional «precedence»` where
 «precedence» := parser! " : " >> precedenceLit
@ -19,17 +14,20 @@ Expand `optional «precedence»` where
 maxSymbol := parser! nonReservedSymbol "max" -/
 def expandOptPrecedence (stx : Syntax) : Option Nat :=
 if stx.isNone then none
-else match ((stx.getArg 0).getArg 1).isNatLit? with
+else match stx[0][1].isNatLit? with
  | some v => some v
  | _      => some Parser.maxPrec

-private def mkParserSeq (ds : Array Syntax) : TermElabM Syntax :=
+private def mkParserSeq (ds : Array Syntax) : TermElabM Syntax := do
 if ds.size == 0 then
  throwUnsupportedSyntax
 else if ds.size == 1 then
-  pure $ ds.get! 0
+  pure ds[0]
 else
-  ds.foldlFromM (fun r d => `(ParserDescr.andthen $r $d)) (ds.get! 0) 1
+  let r := ds[0]
+  for d in ds[1:ds.size] do
+    r ← `(ParserDescr.andthen $r $d)
+  return r

 structure ToParserDescrContext :=
 (catName              : Name)
@ -50,15 +48,15 @@ withReader (fun ctx => { ctx with first := false }) x
 withReader (fun ctx => { ctx with leftRec := false }) x

 def checkLeftRec (stx : Syntax) : ToParserDescrM Bool := do
-ctx ← read;
-if ctx.first && stx.getKind == `Lean.Parser.Syntax.cat then do
-  let cat := (stx.getIdAt 0).eraseMacroScopes;
-  if cat == ctx.catName then do
-    let prec? : Option Nat  := expandOptPrecedence (stx.getArg 1);
-    unless prec?.isNone $ throwErrorAt (stx.getArg 1) ("invalid occurrence of ':<num>' modifier in head");
-    unless ctx.leftRec $
-      throwErrorAt (stx.getArg 3) ("invalid occurrence of '" ++ cat ++ "', parser algorithm does not allow this form of left recursion");
-    markAsTrailingParser; -- mark as trailing par
+let ctx ← read
+if ctx.first && stx.getKind == `Lean.Parser.Syntax.cat then
+  let cat := stx[0].getId.eraseMacroScopes
+  if cat == ctx.catName then
+    let prec? : Option Nat  := expandOptPrecedence stx[1]
+    unless prec?.isNone do throwErrorAt stx[1] ("invalid occurrence of ':<num>' modifier in head")
+    unless ctx.leftRec do
+      throwErrorAt! stx[3] "invalid occurrence of '{cat}', parser algorithm does not allow this form of left recursion"
+    markAsTrailingParser -- mark as trailing par
    pure true
  else
    pure false
@ -66,37 +64,36 @@ else
  pure false

 partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
-| stx =>
-  let kind := stx.getKind;
-  if kind == nullKind then do
-    let args := stx.getArgs;
-    condM (checkLeftRec (stx.getArg 0))
-      (do
-        when (args.size == 1) $ throwErrorAt stx "invalid atomic left recursive syntax";
-        let args := args.eraseIdx 0;
-        args ← args.mapIdxM $ fun i arg => withNotFirst $ toParserDescrAux arg;
-        liftM $ mkParserSeq args)
-      (do
-        args ← args.mapIdxM $ fun i arg => withNotFirst $ toParserDescrAux arg;
-        liftM $ mkParserSeq args)
-  else if kind == choiceKind then do
-    toParserDescrAux (stx.getArg 0)
+| stx => do
+  let kind := stx.getKind
+  if kind == nullKind then
+    let args := stx.getArgs
+    if (← checkLeftRec stx[0]) then
+      if args.size == 1 then throwErrorAt stx "invalid atomic left recursive syntax"
+      let args := args.eraseIdx 0
+      let args ← args.mapIdxM fun i arg => withNotFirst $ toParserDescrAux arg
+      mkParserSeq args
+    else
+      let args ← args.mapIdxM fun i arg => withNotFirst $ toParserDescrAux arg
+      mkParserSeq args
+  else if kind == choiceKind then
+    toParserDescrAux stx[0]
  else if kind == `Lean.Parser.Syntax.paren then
-    toParserDescrAux (stx.getArg 1)
-  else if kind == `Lean.Parser.Syntax.cat then do
-    let cat := (stx.getIdAt 0).eraseMacroScopes;
-    ctx ← read;
+    toParserDescrAux stx[1]
+  else if kind == `Lean.Parser.Syntax.cat then
+    let cat := stx[0].getId.eraseMacroScopes
+    let ctx ← read
    if ctx.first && cat == ctx.catName then
      throwErrorAt stx "invalid atomic left recursive syntax"
-    else do
-      let prec? : Option Nat  := expandOptPrecedence (stx.getArg 1);
-      env ← getEnv;
+    else
+      let prec? : Option Nat  := expandOptPrecedence stx[1]
+      let env ← getEnv
      if Parser.isParserCategory env cat then
-        let prec := prec?.getD 0;
+        let prec := prec?.getD 0
        `(ParserDescr.cat $(quote cat) $(quote prec))
-      else do
+      else
        -- `cat` is not a valid category name. Thus, we test whether it is a valid constant
-        candidates ← resolveGlobalConst cat;
+        let candidates ← resolveGlobalConst cat
        let candidates := candidates.filter fun c =>
            match env.find? c with
            | none      => false
@ -106,18 +103,17 @@ partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
              | Expr.const `Lean.Parser.Parser _ _         => true
              | Expr.const `Lean.ParserDescr _ _           => true
              | Expr.const `Lean.TrailingParserDescr _ _   => true
-              | _                                          => false;
+              | _                                          => false
         match candidates with
-         | []  => throwErrorAt (stx.getArg 3) ("unknown category '" ++ cat ++ "' or parser declaration")
-         | [c] => do
-           unless prec?.isNone $ throwErrorAt (stx.getArg 3) "unexpected precedence";
+         | []  => throwErrorAt! stx[3] "unknown category '{cat}' or parser declaration"
+         | [c] =>
+           unless prec?.isNone do throwErrorAt stx[3] "unexpected precedence"
           `(ParserDescr.parser $(quote c))
-         | cs  => throwErrorAt (stx.getArg 3) ("ambiguous parser declaration " ++ toString cs)
-  else if kind == `Lean.Parser.Syntax.atom then do
-    match (stx.getArg 0).isStrLit? with
-    | some atom => do
-      ctx ← read;
-      if ctx.leadingIdentAsSymbol then
+         | cs  => throwErrorAt! stx[3] "ambiguous parser declaration {cs}"
+  else if kind == `Lean.Parser.Syntax.atom then
+    match stx[0].isStrLit? with
+    | some atom =>
+      if (← read).leadingIdentAsSymbol then
        `(ParserDescr.nonReservedSymbol $(quote atom) false)
      else
        `(ParserDescr.symbol $(quote atom))
@ -132,52 +128,52 @@ partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
    `(ParserDescr.ident)
  else if kind == `Lean.Parser.Syntax.noWs then
    `(ParserDescr.noWs)
-  else if kind == `Lean.Parser.Syntax.try then do
-    d ← withoutLeftRec $ toParserDescrAux (stx.getArg 1);
+  else if kind == `Lean.Parser.Syntax.try then
+    let d ← withoutLeftRec $ toParserDescrAux stx[1]
    `(ParserDescr.try $d)
-  else if kind == `Lean.Parser.Syntax.notFollowedBy then do
-    d ← withoutLeftRec $ toParserDescrAux (stx.getArg 1);
+  else if kind == `Lean.Parser.Syntax.notFollowedBy then
+    let d ← withoutLeftRec $ toParserDescrAux stx[1]
    `(ParserDescr.notFollowedBy $d)
-  else if kind == `Lean.Parser.Syntax.lookahead then do
-    d ← withoutLeftRec $ toParserDescrAux (stx.getArg 1);
+  else if kind == `Lean.Parser.Syntax.lookahead then
+    let d ← withoutLeftRec $ toParserDescrAux stx[1]
    `(ParserDescr.lookahead $d)
-  else if kind == `Lean.Parser.Syntax.interpolatedStr then do
-    d ← withoutLeftRec $ toParserDescrAux (stx.getArg 1);
+  else if kind == `Lean.Parser.Syntax.interpolatedStr then
+    let d ← withoutLeftRec $ toParserDescrAux stx[1]
    `(ParserDescr.interpolatedStr $d)
-  else if kind == `Lean.Parser.Syntax.sepBy then do
-    d₁ ← withoutLeftRec $ toParserDescrAux (stx.getArg 1);
-    d₂ ← withoutLeftRec $ toParserDescrAux (stx.getArg 2);
+  else if kind == `Lean.Parser.Syntax.sepBy then
+    let d₁ ← withoutLeftRec $ toParserDescrAux stx[1]
+    let d₂ ← withoutLeftRec $ toParserDescrAux stx[2]
    `(ParserDescr.sepBy $d₁ $d₂)
-  else if kind == `Lean.Parser.Syntax.sepBy1 then do
-    d₁ ← withoutLeftRec $ toParserDescrAux (stx.getArg 1);
-    d₂ ← withoutLeftRec $ toParserDescrAux (stx.getArg 2);
+  else if kind == `Lean.Parser.Syntax.sepBy1 then
+    let d₁ ← withoutLeftRec $ toParserDescrAux stx[1]
+    let d₂ ← withoutLeftRec $ toParserDescrAux stx[2]
    `(ParserDescr.sepBy1 $d₁ $d₂)
-  else if kind == `Lean.Parser.Syntax.many then do
-    d ← withoutLeftRec $ toParserDescrAux (stx.getArg 0);
+  else if kind == `Lean.Parser.Syntax.many then
+    let d ← withoutLeftRec $ toParserDescrAux stx[0]
    `(ParserDescr.many $d)
-  else if kind == `Lean.Parser.Syntax.many1 then do
-    d ← withoutLeftRec $ toParserDescrAux (stx.getArg 0);
+  else if kind == `Lean.Parser.Syntax.many1 then
+    let d ← withoutLeftRec $ toParserDescrAux stx[0]
    `(ParserDescr.many1 $d)
-  else if kind == `Lean.Parser.Syntax.optional then do
-    d ← withoutLeftRec $ toParserDescrAux (stx.getArg 0);
+  else if kind == `Lean.Parser.Syntax.optional then
+    let d ← withoutLeftRec $ toParserDescrAux stx[0]
    `(ParserDescr.optional $d)
-  else if kind == `Lean.Parser.Syntax.orelse then do
-    d₁ ← withoutLeftRec $ toParserDescrAux (stx.getArg 0);
-    d₂ ← withoutLeftRec $ toParserDescrAux (stx.getArg 2);
+  else if kind == `Lean.Parser.Syntax.orelse then
+    let d₁ ← withoutLeftRec $ toParserDescrAux stx[0]
+    let d₂ ← withoutLeftRec $ toParserDescrAux stx[2]
    `(ParserDescr.orelse $d₁ $d₂)
-  else do
-    stxNew? ← liftM (liftMacroM (expandMacro? stx) : TermElabM _);
+  else
+    let stxNew? ← liftM (liftMacroM (expandMacro? stx) : TermElabM _)
    match stxNew? with
    | some stxNew => toParserDescrAux stxNew
-    | none => throwErrorAt stx $ "unexpected syntax kind of category `syntax`: " ++ kind
+    | none => throwErrorAt! stx "unexpected syntax kind of category `syntax`: {kind}"

 /--
  Given a `stx` of category `syntax`, return a pair `(newStx, trailingParser)`,
  where `newStx` is of category `term`. After elaboration, `newStx` should have type
  `TrailingParserDescr` if `trailingParser == true`, and `ParserDescr` otherwise. -/
 def toParserDescr (stx : Syntax) (catName : Name) : TermElabM (Syntax × Bool) := do
-env ← getEnv;
-let leadingIdentAsSymbol := Parser.leadingIdentAsSymbol env catName;
+let env ← getEnv
+let leadingIdentAsSymbol := Parser.leadingIdentAsSymbol env catName
 (toParserDescrAux stx { catName := catName, first := true, leftRec := true, leadingIdentAsSymbol := leadingIdentAsSymbol }).run false

 end Term
@ -190,55 +186,59 @@ match catName with
 | _              => unreachable!

 private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := do
-let quotSymbol := "`(" ++ getCatSuffix catName ++ "|";
-let kind := catName ++ `quot;
-cmd ← `(@[termParser] def $(mkIdent kind) : Lean.ParserDescr := Lean.ParserDescr.node $(quote kind) $(quote Lean.Parser.maxPrec) (Lean.ParserDescr.andthen (Lean.ParserDescr.symbol $(quote quotSymbol)) (Lean.ParserDescr.andthen (Lean.ParserDescr.cat $(quote catName) 0) (Lean.ParserDescr.symbol ")"))));
+let quotSymbol := "`(" ++ getCatSuffix catName ++ "|"
+let kind := catName ++ `quot
+let cmd ← `(
+  @[termParser] def $(mkIdent kind) : Lean.ParserDescr :=
+    Lean.ParserDescr.node $(quote kind) $(quote Lean.Parser.maxPrec)
+      (Lean.ParserDescr.andthen (Lean.ParserDescr.symbol $(quote quotSymbol))
+        (Lean.ParserDescr.andthen (Lean.ParserDescr.cat $(quote catName) 0) (Lean.ParserDescr.symbol ")"))))
 elabCommand cmd

@[builtinCommandElab syntaxCat] def elabDeclareSyntaxCat : CommandElab :=
 fun stx => do
-  let catName  := stx.getIdAt 1;
-  let attrName := catName.appendAfter "Parser";
-  env ← getEnv;
-  env ← liftIO $ Parser.registerParserCategory env attrName catName;
-  setEnv env;
+  let catName  := stx[1].getId
+  let attrName := catName.appendAfter "Parser"
+  let env ← getEnv
+  let env ← liftIO $ Parser.registerParserCategory env attrName catName
+  setEnv env
  declareSyntaxCatQuotParser catName

 def mkKindName (catName : Name) : Name :=
 `_kind ++ catName

 def mkFreshKind (catName : Name) : CommandElabM Name := do
-scp ← getCurrMacroScope;
-mainModule ← getMainModule;
+let scp ← getCurrMacroScope
+let mainModule ← getMainModule
 pure $ Lean.addMacroScope mainModule (mkKindName catName) scp

 def Macro.mkFreshKind (catName : Name) : MacroM Name :=
 Macro.addMacroScope (mkKindName catName)

 def mkKind (stx : Syntax) : CommandElabM Name := do
-let kind := stx.getId;
+let kind := stx.getId
 if kind.hasMacroScopes then
  pure kind
-else do
-  currNamespace ← getCurrNamespace;
+else
+  let currNamespace ← getCurrNamespace
  pure (currNamespace ++ kind)

 private def elabKindPrio (stx : Syntax) (catName : Name) : CommandElabM (Name × Nat) := do
-if stx.isNone then do
-  k ← mkFreshKind catName;
+if stx.isNone then
+  let k ← mkFreshKind catName
  pure (k, 0)
 else
-  let arg := stx.getArg 1;
-  if arg.getKind == `Lean.Parser.Command.parserKind then do
-    k ← mkKind (arg.getArg 0);
+  let arg := stx[1]
+  if arg.getKind == `Lean.Parser.Command.parserKind then
+    let k ← mkKind arg[0]
    pure (k, 0)
-  else if arg.getKind == `Lean.Parser.Command.parserPrio then do
-    k ← mkFreshKind catName;
-    let prio := (arg.getArg 0).isNatLit?.getD 0;
+  else if arg.getKind == `Lean.Parser.Command.parserPrio then
+    let k ← mkFreshKind catName
+    let prio := arg[0].isNatLit?.getD 0
    pure (k, prio)
-  else if arg.getKind == `Lean.Parser.Command.parserKindPrio then do
-    k ← mkKind (arg.getArg 0);
-    let prio := (arg.getArg 2).isNatLit?.getD 0;
+  else if arg.getKind == `Lean.Parser.Command.parserKindPrio then
+    let k ← mkKind arg[0]
+    let prio := arg[2].isNatLit?.getD 0
    pure (k, prio)
  else
    throwError "unexpected syntax kind/priority"
@ -253,13 +253,13 @@ else
 -/
 private partial def isAtomLikeSyntax : Syntax → Bool
 | stx =>
-  let kind := stx.getKind;
+  let kind := stx.getKind
  if kind == nullKind then
-    isAtomLikeSyntax (stx.getArg 0) && isAtomLikeSyntax (stx.getArg (stx.getNumArgs - 1))
+    isAtomLikeSyntax stx[0] && isAtomLikeSyntax stx[stx.getNumArgs - 1]
  else if kind == choiceKind then
-    isAtomLikeSyntax (stx.getArg 0) -- see toParserDescrAux
+    isAtomLikeSyntax stx[0] -- see toParserDescrAux
  else if kind == `Lean.Parser.Syntax.paren then
-    isAtomLikeSyntax (stx.getArg 1)
+    isAtomLikeSyntax stx[1]
  else
    kind == `Lean.Parser.Syntax.atom

@ -268,22 +268,24 @@ def «syntax»      := parser! "syntax " >> optPrecedence >> optKindPrio >> many
 -/
@[builtinCommandElab «syntax»] def elabSyntax : CommandElab :=
 fun stx => do
-  env ← getEnv;
-  let cat := (stx.getIdAt 5).eraseMacroScopes;
-  unless (Parser.isParserCategory env cat) $ throwErrorAt (stx.getArg 5) ("unknown category '" ++ cat ++ "'");
-  let syntaxParser := stx.getArg 3;
+  let env ← getEnv
+  let cat := stx[5].getId.eraseMacroScopes
+  unless (Parser.isParserCategory env cat) do throwErrorAt stx[5] ("unknown category '" ++ cat ++ "'")
+  let syntaxParser := stx[3]
  -- If the user did not provide an explicit precedence, we assign `maxPrec` to atom-like syntax and `leadPrec` otherwise.
-  let precDefault  := if isAtomLikeSyntax syntaxParser then Parser.maxPrec else Parser.leadPrec;
-  let prec := (Term.expandOptPrecedence (stx.getArg 1)).getD precDefault;
-  (kind, prio) ← elabKindPrio (stx.getArg 2) cat;
-  let catParserId := mkIdentFrom stx (cat.appendAfter "Parser");
-  (val, trailingParser) ← runTermElabM none $ fun _ => Term.toParserDescr syntaxParser cat;
-  d ←
+  let precDefault  := if isAtomLikeSyntax syntaxParser then Parser.maxPrec else Parser.leadPrec
+  let prec := (Term.expandOptPrecedence stx[1]).getD precDefault
+  let (kind, prio) ← elabKindPrio stx[2] cat
+  let catParserId := mkIdentFrom stx (cat.appendAfter "Parser")
+  let (val, trailingParser) ← runTermElabM none fun _ => Term.toParserDescr syntaxParser cat
+  let d ←
    if trailingParser then
-      `(@[$catParserId:ident $(quote prio):numLit] def $(mkIdentFrom stx kind) : Lean.TrailingParserDescr := ParserDescr.trailingNode $(quote kind) $(quote prec) $val)
+      `(@[$catParserId:ident $(quote prio):numLit] def $(mkIdentFrom stx kind) : Lean.TrailingParserDescr :=
+         ParserDescr.trailingNode $(quote kind) $(quote prec) $val)
    else
-      `(@[$catParserId:ident $(quote prio):numLit] def $(mkIdentFrom stx kind) : Lean.ParserDescr := ParserDescr.node $(quote kind) $(quote prec) $val);
-  trace `Elab fun _ => d;
+      `(@[$catParserId:ident $(quote prio):numLit] def $(mkIdentFrom stx kind) : Lean.ParserDescr :=
+         ParserDescr.node $(quote kind) $(quote prec) $val)
+  trace `Elab fun _ => d
  withMacroExpansion stx d $ elabCommand d

 /-
@ -291,50 +293,50 @@ def syntaxAbbrev  := parser! "syntax " >> ident >> " := " >> many1 syntaxParser
 -/
@[builtinCommandElab «syntaxAbbrev»] def elabSyntaxAbbrev : CommandElab :=
 fun stx => do
-  let declName := stx.getArg 1;
-  (val, _) ← runTermElabM none $ fun _ => Term.toParserDescr (stx.getArg 3) Name.anonymous;
-  stx' ← `(def $declName : Lean.ParserDescr := $val);
+  let declName := stx[1]
+  let (val, _) ← runTermElabM none $ fun _ => Term.toParserDescr stx[3] Name.anonymous
+  let stx' ← `(def $declName : Lean.ParserDescr := $val)
  withMacroExpansion stx stx' $ elabCommand stx'

 def elabMacroRulesAux (k : SyntaxNodeKind) (alts : Array Syntax) : CommandElabM Syntax := do
-alts ← alts.mapSepElemsM $ fun alt => do {
-  let lhs := alt.getArg 0;
-  let pat := lhs.getArg 0;
-  when (!pat.isQuot) $
-    throwUnsupportedSyntax;
-  let quot := pat.getArg 1;
-  let k' := quot.getKind;
+alts ← alts.mapSepElemsM fun alt => do
+  let lhs := alt[0]
+  let pat := lhs[0]
+  if !pat.isQuot then
+    throwUnsupportedSyntax
+  let quot := pat[1]
+  let k' := quot.getKind
  if k' == k then
    pure alt
-  else if k' == choiceKind then do
-     match quot.getArgs.find? $ fun quotAlt => quotAlt.getKind == k with
-     | none      => throwErrorAt alt ("invalid macro_rules alternative, expected syntax node kind '" ++ k ++ "'")
-     | some quot => do
-       let pat := pat.setArg 1 quot;
-       let lhs := lhs.setArg 0 pat;
+  else if k' == choiceKind then
+     match quot.getArgs.find? fun quotAlt => quotAlt.getKind == k with
+     | none      => throwErrorAt! alt "invalid macro_rules alternative, expected syntax node kind '{k}'"
+     | some quot =>
+       let pat := pat.setArg 1 quot
+       let lhs := lhs.setArg 0 pat
       pure $ alt.setArg 0 lhs
  else
-    throwErrorAt alt ("invalid macro_rules alternative, unexpected syntax node kind '" ++ k' ++ "'")
-};
-`(@[macro $(Lean.mkIdent k)] def myMacro : Macro := fun stx => match_syntax stx with $alts:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
+    throwErrorAt! alt "invalid macro_rules alternative, unexpected syntax node kind '{k'}'"
+`(@[macro $(Lean.mkIdent k)] def myMacro : Macro :=
+   fun stx => match_syntax stx with $alts:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax)

 def inferMacroRulesAltKind (alt : Syntax) : CommandElabM SyntaxNodeKind := do
-let lhs := alt.getArg 0;
-let pat := lhs.getArg 0;
-when (!pat.isQuot) $
-  throwUnsupportedSyntax;
-let quot := pat.getArg 1;
+let lhs := alt[0]
+let pat := lhs[0]
+if !pat.isQuot then
+  throwUnsupportedSyntax
+let quot := pat[1]
 pure quot.getKind

 def elabNoKindMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
-k ← inferMacroRulesAltKind (alts.get! 0);
+let k ← inferMacroRulesAltKind (alts.get! 0)
 if k == choiceKind then
-  throwErrorAt (alts.get! 0)
+  throwErrorAt! alts[0]
    "invalid macro_rules alternative, multiple interpretations for pattern (solution: specify node kind using `macro_rules [<kind>] ...`)"
-else do
-  altsK    ← alts.filterSepElemsM (fun alt => do k' ← inferMacroRulesAltKind alt; pure $ k == k');
-  altsNotK ← alts.filterSepElemsM (fun alt => do k' ← inferMacroRulesAltKind alt; pure $ k != k');
-  defCmd   ← elabMacroRulesAux k altsK;
+else
+  let altsK    ← alts.filterSepElemsM fun alt => do pure $ k == (← inferMacroRulesAltKind alt)
+  let altsNotK ← alts.filterSepElemsM fun alt => do pure $ k != (← inferMacroRulesAltKind alt)
+  let defCmd   ← elabMacroRulesAux k altsK
  if altsNotK.isEmpty then
    pure defCmd
  else
@ -344,8 +346,8 @@ else do
 adaptExpander $ fun stx => match_syntax stx with
 | `(macro_rules $alts:matchAlt*)           => elabNoKindMacroRulesAux alts
 | `(macro_rules | $alts:matchAlt*)         => elabNoKindMacroRulesAux alts
-| `(macro_rules [$kind] $alts:matchAlt*)   => do k ← mkKind kind; elabMacroRulesAux k alts
-| `(macro_rules [$kind] | $alts:matchAlt*) => do k ← mkKind kind; elabMacroRulesAux k alts
+| `(macro_rules [$kind] $alts:matchAlt*)   => do elabMacroRulesAux (← mkKind kind) alts
+| `(macro_rules [$kind] | $alts:matchAlt*) => do elabMacroRulesAux (← mkKind kind) alts
 | _                                        => throwUnsupportedSyntax

@[builtinMacro Lean.Parser.Command.mixfix] def expandMixfix : Macro :=
@ -366,16 +368,16 @@ private partial def antiquote (vars : Array Syntax) : Syntax → Syntax
  else
    stx
 | _ => match stx with
-  | Syntax.node k args => Syntax.node k (args.map antiquote)
+  | Syntax.node k args => Syntax.node k (args.map (antiquote vars))
  | stx => stx

 /- Convert `notation` command lhs item into a `syntax` command item -/
 def expandNotationItemIntoSyntaxItem (stx : Syntax) : MacroM Syntax :=
-let k := stx.getKind;
+let k := stx.getKind
 if k == `Lean.Parser.Command.identPrec then
-  pure $ Syntax.node `Lean.Parser.Syntax.cat #[mkIdentFrom stx `term,  stx.getArg 1]
+  pure $ Syntax.node `Lean.Parser.Syntax.cat #[mkIdentFrom stx `term,  stx[1]]
 else if k == quotedSymbolKind then
-  match stx.getArg 1 with
+  match stx[1] with
  | Syntax.atom info val => pure $ Syntax.node `Lean.Parser.Syntax.atom #[mkStxStrLit val info]
  | _                    => Macro.throwUnsupported
 else if k == strLitKind then
@ -390,28 +392,28 @@ match stx.isStrLit? with

 /- Convert `notation` command lhs item a pattern element -/
 def expandNotationItemIntoPattern (stx : Syntax) : MacroM Syntax :=
-let k := stx.getKind;
+let k := stx.getKind
 if k == `Lean.Parser.Command.identPrec then
-  let item := stx.getArg 0;
+  let item := stx[0]
  pure $ mkNode `antiquot #[mkAtom "$", mkNullNode, item, mkNullNode, mkNullNode]
 else if k == quotedSymbolKind then
-  pure $ stx.getArg 1
+  pure stx[1]
 else if k == strLitKind then
  strLitToPattern stx
 else
  Macro.throwUnsupported

 private def expandNotationAux (ref : Syntax) (prec? : Option Syntax) (items : Array Syntax) (rhs : Syntax) : MacroM Syntax := do
-kind ← Macro.mkFreshKind `term;
+let kind ← Macro.mkFreshKind `term
 -- build parser
-syntaxParts ← items.mapM expandNotationItemIntoSyntaxItem;
-let cat := mkIdentFrom ref `term;
+let syntaxParts ← items.mapM expandNotationItemIntoSyntaxItem
+let cat := mkIdentFrom ref `term
 -- build macro rules
-let vars := items.filter $ fun item => item.getKind == `Lean.Parser.Command.identPrec;
-let vars := vars.map $ fun var => var.getArg 0;
-let rhs := antiquote vars rhs;
-patArgs ← items.mapM expandNotationItemIntoPattern;
-let pat := Syntax.node kind patArgs;
+let vars := items.filter fun item => item.getKind == `Lean.Parser.Command.identPrec
+let vars := vars.map fun var => var[0]
+let rhs := antiquote vars rhs
+let patArgs ← items.mapM expandNotationItemIntoPattern
+let pat := Syntax.node kind patArgs
 match prec? with
 | none      => `(syntax [$(mkIdentFrom ref kind):ident] $syntaxParts* : $cat macro_rules | `($pat) => `($rhs))
 | some prec => `(syntax:$prec [$(mkIdentFrom ref kind):ident] $syntaxParts* : $cat macro_rules | `($pat) => `($rhs))
@ -425,9 +427,9 @@ match_syntax stx with

 /- Convert `macro` argument into a `syntax` command item -/
 def expandMacroArgIntoSyntaxItem (stx : Syntax) : MacroM Syntax :=
-let k := stx.getKind;
+let k := stx.getKind
 if k == `Lean.Parser.Command.macroArgSimple then
-  pure $ stx.getArg 2
+  pure stx[2]
 else if k == strLitKind then
  pure $ Syntax.node `Lean.Parser.Syntax.atom #[stx]
 else
@ -436,17 +438,17 @@ else
 /- Convert `macro` head into a `syntax` command item -/
 def expandMacroHeadIntoSyntaxItem (stx : Syntax) : MacroM Syntax :=
 if stx.isIdent then
-  let info := stx.getHeadInfo.getD {};
-  let id   := stx.getId;
+  let info := stx.getHeadInfo.getD {}
+  let id   := stx.getId
  pure $ Syntax.node `Lean.Parser.Syntax.atom #[mkStxStrLit (toString id) info]
 else
  expandMacroArgIntoSyntaxItem stx

 /- Convert `macro` arg into a pattern element -/
 def expandMacroArgIntoPattern (stx : Syntax) : MacroM Syntax :=
-let k := stx.getKind;
+let k := stx.getKind
 if k == `Lean.Parser.Command.macroArgSimple then
-  let item := stx.getArg 0;
+  let item := stx[0]
  pure $ mkNode `antiquot #[mkAtom "$", mkNullNode, item, mkNullNode, mkNullNode]
 else if k == strLitKind then
  strLitToPattern stx
@ -462,36 +464,38 @@ else

@[builtinMacro Lean.Parser.Command.macro] def expandMacro : Macro :=
 fun stx => do
-  let prec := (stx.getArg 1).getArgs;
-  let head := stx.getArg 2;
-  let args := (stx.getArg 3).getArgs;
-  let cat  := stx.getArg 5;
-  kind ← Macro.mkFreshKind (cat.getId).eraseMacroScopes;
+  let prec := stx[1].getArgs
+  let head := stx[2]
+  let args := stx[3].getArgs
+  let cat  := stx[5]
+  let kind ← Macro.mkFreshKind (cat.getId).eraseMacroScopes
  -- build parser
-  stxPart  ← expandMacroHeadIntoSyntaxItem head;
-  stxParts ← args.mapM expandMacroArgIntoSyntaxItem;
-  let stxParts := #[stxPart] ++ stxParts;
+  let stxPart  ← expandMacroHeadIntoSyntaxItem head
+  let stxParts ← args.mapM expandMacroArgIntoSyntaxItem
+  let stxParts := #[stxPart] ++ stxParts
  -- build macro rules
-  patHead ← expandMacroHeadIntoPattern head;
-  patArgs ← args.mapM expandMacroArgIntoPattern;
-  let pat := Syntax.node kind (#[patHead] ++ patArgs);
+  let patHead ← expandMacroHeadIntoPattern head
+  let patArgs ← args.mapM expandMacroArgIntoPattern
+  let pat := Syntax.node kind (#[patHead] ++ patArgs)
  if stx.getArgs.size == 8 then
    -- `stx` is of the form `macro $head $args* : $cat => term`
-    let rhs := stx.getArg 7;
-    `(syntax $prec* [$(mkIdentFrom stx kind):ident] $stxParts* : $cat macro_rules | `($pat) => $rhs)
+    let rhs := stx[7]
+    `(syntax $prec* [$(mkIdentFrom stx kind):ident] $stxParts* : $cat
+      macro_rules | `($pat) => $rhs)
  else
    -- `stx` is of the form `macro $head $args* : $cat => `( $body )`
-    let rhsBody := stx.getArg 8;
-    `(syntax $prec* [$(mkIdentFrom stx kind):ident] $stxParts* : $cat macro_rules | `($pat) => `($rhsBody))
+    let rhsBody := stx[8]
+    `(syntax $prec* [$(mkIdentFrom stx kind):ident] $stxParts* : $cat
+      macro_rules | `($pat) => `($rhsBody))

@[init] private def regTraceClasses : IO Unit := do
-registerTraceClass `Elab.syntax;
+registerTraceClass `Elab.syntax
 pure ()

@[inline] def withExpectedType (expectedType? : Option Expr) (x : Expr → TermElabM Expr) : TermElabM Expr := do
-Term.tryPostponeIfNoneOrMVar expectedType?;
-some expectedType ← pure expectedType?
-  | throwError "expected type must be known";
+Term.tryPostponeIfNoneOrMVar expectedType?
+let some expectedType ← pure expectedType?
+  | throwError "expected type must be known"
 x expectedType

 /-
@ -500,41 +504,55 @@ parser! "elab " >> optPrecedence >> elabHead >> many elabArg >> elabTail
 -/
@[builtinMacro Lean.Parser.Command.elab] def expandElab : Macro :=
 fun stx => do
-  let ref := stx;
-  let prec    := (stx.getArg 1).getArgs;
-  let head    := stx.getArg 2;
-  let args    := (stx.getArg 3).getArgs;
-  let cat     := stx.getArg 5;
-  let expectedTypeSpec := stx.getArg 6;
-  let rhs     := stx.getArg 8;
-  let catName := cat.getId;
-  kind ← Macro.mkFreshKind catName.eraseMacroScopes;
+  let ref := stx
+  let prec    := stx[1].getArgs
+  let head    := stx[2]
+  let args    := stx[3].getArgs
+  let cat     := stx[5]
+  let expectedTypeSpec := stx[6]
+  let rhs     := stx[8]
+  let catName := cat.getId
+  let kind ← Macro.mkFreshKind catName.eraseMacroScopes
  -- build parser
-  stxPart  ← expandMacroHeadIntoSyntaxItem head;
-  stxParts ← args.mapM expandMacroArgIntoSyntaxItem;
-  let stxParts := #[stxPart] ++ stxParts;
+  let stxPart  ← expandMacroHeadIntoSyntaxItem head
+  let stxParts ← args.mapM expandMacroArgIntoSyntaxItem
+  let stxParts := #[stxPart] ++ stxParts
  -- build pattern for `martch_syntax
-  patHead ← expandMacroHeadIntoPattern head;
-  patArgs ← args.mapM expandMacroArgIntoPattern;
-  let pat := Syntax.node kind (#[patHead] ++ patArgs);
-  let kindId    := mkIdentFrom ref kind;
+  let patHead ← expandMacroHeadIntoPattern head
+  let patArgs ← args.mapM expandMacroArgIntoPattern
+  let pat := Syntax.node kind (#[patHead] ++ patArgs)
+  let kindId    := mkIdentFrom ref kind
  if expectedTypeSpec.hasArgs then
    if catName == `term then
-      let expId := expectedTypeSpec.getArg 1;
-      `(syntax $prec* [$kindId:ident] $stxParts* : $cat @[termElab $kindId:ident] def elabFn : Lean.Elab.Term.TermElab := fun stx expectedType? => match_syntax stx with | `($pat) => Lean.Elab.Command.withExpectedType expectedType? fun $expId => $rhs | _ => throwUnsupportedSyntax)
+      let expId := expectedTypeSpec[1]
+      `(syntax $prec* [$kindId:ident] $stxParts* : $cat
+        @[termElab $kindId:ident] def elabFn : Lean.Elab.Term.TermElab :=
+        fun stx expectedType? => match_syntax stx with
+          | `($pat) => Lean.Elab.Command.withExpectedType expectedType? fun $expId => $rhs
+          | _ => throwUnsupportedSyntax)
    else
-      Macro.throwError expectedTypeSpec ("syntax category '" ++ toString catName ++ "' does not support expected type specification")
+      Macro.throwError expectedTypeSpec s!"syntax category '{catName}' does not support expected type specification"
  else if catName == `term then
-    `(syntax $prec* [$kindId:ident] $stxParts* : $cat @[termElab $kindId:ident] def elabFn : Lean.Elab.Term.TermElab := fun stx _ => match_syntax stx with | `($pat) => $rhs | _ => throwUnsupportedSyntax)
+    `(syntax $prec* [$kindId:ident] $stxParts* : $cat
+      @[termElab $kindId:ident] def elabFn : Lean.Elab.Term.TermElab :=
+      fun stx _ => match_syntax stx with
+        | `($pat) => $rhs
+        | _ => throwUnsupportedSyntax)
  else if catName == `command then
-    `(syntax $prec* [$kindId:ident] $stxParts* : $cat @[commandElab $kindId:ident] def elabFn : Lean.Elab.Command.CommandElab := fun stx => match_syntax stx with | `($pat) => $rhs | _ => throwUnsupportedSyntax)
+    `(syntax $prec* [$kindId:ident] $stxParts* : $cat
+      @[commandElab $kindId:ident] def elabFn : Lean.Elab.Command.CommandElab :=
+      fun stx => match_syntax stx with
+        | `($pat) => $rhs
+        | _ => throwUnsupportedSyntax)
  else if catName == `tactic then
-    `(syntax $prec* [$kindId:ident] $stxParts* : $cat @[tactic $kindId:ident] def elabFn : Lean.Elab.Tactic.Tactic := fun stx => match_syntax stx with | `(tactic|$pat) => $rhs | _ => throwUnsupportedSyntax)
+    `(syntax $prec* [$kindId:ident] $stxParts* : $cat
+      @[tactic $kindId:ident] def elabFn : Lean.Elab.Tactic.Tactic :=
+      fun stx => match_syntax stx with
+        | `(tactic|$pat) => $rhs
+        | _ => throwUnsupportedSyntax)
  else
    -- We considered making the command extensible and support new user-defined categories. We think it is unnecessary.
    -- If users want this feature, they add their own `elab` macro that uses this one as a fallback.
-    Macro.throwError ref ("unsupported syntax category '" ++ toString catName ++ "'")
+    Macro.throwError ref s!"unsupported syntax category '{catName}'"

-end Command
-end Elab
-end Lean
+end Lean.Elab.Command
--- a/stage0/src/Lean/Elab/SyntheticMVars.lean
+++ b/stage0/src/Lean/Elab/SyntheticMVars.lean
@ -30,7 +30,7 @@ if val.hasExprMVar then throwError! "tactic failed, result still contain metavar
 def runTactic (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do
 /- Recall, `tacticCode` is the whole `by ...` expression.
   We store the `by` because in the future we want to save the initial state information at the `by` position. -/
-let code := tacticCode.getArg 1
+let code := tacticCode[1]
 modifyThe Meta.State fun s => { s with mctx := s.mctx.instantiateMVarDeclMVars mvarId }
 let remainingGoals ← liftTacticElabM mvarId do evalTactic code; getUnsolvedGoals
 unless remainingGoals.isEmpty do reportUnsolvedGoals remainingGoals
--- a/stage0/src/Lean/Elab/Tactic/Basic.lean
+++ b/stage0/src/Lean/Elab/Tactic/Basic.lean
@ -249,22 +249,22 @@ modifyMCtx fun mctx => do
  pure mctx

@[builtinTactic seq1] def evalSeq1 : Tactic :=
-fun stx => (stx.getArg 0).forSepArgsM evalTactic
+fun stx => stx[0].forSepArgsM evalTactic

@[builtinTactic paren] def evalParen : Tactic :=
-fun stx => evalSeq1 (stx.getArg 1)
+fun stx => evalSeq1 stx[1]

@[builtinTactic tacticSeq1Indented] def evalTacticSeq1Indented : Tactic :=
-fun stx => stx.getArg 0 $.forArgsM fun seqElem => evalTactic (seqElem.getArg 0)
+fun stx => stx[0].forArgsM fun seqElem => evalTactic seqElem[0]

@[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic :=
-fun stx => withRef (stx.getArg 2) $ focus $ stx.getArg 1 $.forArgsM fun seqElem => evalTactic (seqElem.getArg 0)
+fun stx => withRef stx[2] $ focus $ stx[1].forArgsM fun seqElem => evalTactic seqElem[0]

@[builtinTactic Parser.Tactic.focus] def evalFocus : Tactic :=
-fun stx => focus $ evalTactic (stx.getArg 1)
+fun stx => focus $ evalTactic stx[1]

@[builtinTactic tacticSeq] def evalTacticSeq : Tactic :=
-fun stx => evalTactic (stx.getArg 0)
+fun stx => evalTactic stx[0]

 partial def evalChoiceAux (tactics : Array Syntax) : Nat → TacticM Unit
 | i =>
@ -284,7 +284,7 @@ fun stx => pure ()

@[builtinTactic failIfSuccess] def evalFailIfSuccess : Tactic :=
 fun stx => do
-  let tactic := stx.getArg 1
+  let tactic := stx[1]
  if (← do try evalTactic tactic; pure true catch _ => pure false) then
    throwError "tactic succeeded"

@ -318,7 +318,7 @@ fun stx => match_syntax stx with

@[builtinTactic Lean.Parser.Tactic.introMatch] def evalIntroMatch : Tactic :=
 fun stx => do
-  let matchAlts := stx.getArg 1
+  let matchAlts := stx[1]
  let stxNew ← liftMacroM $ Term.expandMatchAltsIntoMatchTactic stx matchAlts
  withMacroExpansion stx stxNew $ evalTactic stxNew

--- a/stage0/src/Lean/Elab/Tactic/Binders.lean
+++ b/stage0/src/Lean/Elab/Tactic/Binders.lean
@ -24,7 +24,7 @@ fun stx => do

@[builtinMacro Lean.Parser.Tactic.show] def expandShowTactic : Macro :=
 fun stx =>
-  let type := stx.getArg 1
+  let type := stx[1]
  `(tactic| refine (show $type from ?_))

 end Lean.Elab.Tactic
--- a/stage0/src/Lean/Elab/Tactic/Generalize.lean
+++ b/stage0/src/Lean/Elab/Tactic/Generalize.lean
@ -13,11 +13,11 @@ namespace Lean.Elab.Tactic
 open Meta

 private def getAuxHypothesisName (stx : Syntax) : Option Name :=
-if (stx.getArg 1).isNone then none
-else some ((stx.getArg 1).getIdAt 0)
+if stx[1].isNone then none
+else some stx[1][0].getId

 private def getVarName (stx : Syntax) : Name :=
-stx.getIdAt 4
+stx[4].getId

 private def evalGeneralizeFinalize (mvarId : MVarId) (e : Expr) (target : Expr) : MetaM (List MVarId) := do
 let tag    ← Meta.getMVarTag mvarId
@ -68,7 +68,7 @@ match h? with
 fun stx => do
  let h? := getAuxHypothesisName stx
  let x  := getVarName stx
-  let e ← elabTerm (stx.getArg 2) none
+  let e ← elabTerm stx[2] none
  evalGeneralizeAux h? e x

 end Lean.Elab.Tactic
--- a/stage0/src/Lean/Elab/Tactic/Induction.lean
+++ b/stage0/src/Lean/Elab/Tactic/Induction.lean
@ -17,13 +17,13 @@ open Meta
 -- Recall that
 -- majorPremise := parser! optional (try (ident >> " : ")) >> termParser
 private def getAuxHypothesisName (stx : Syntax) : Option Name :=
-if stx.getArg 1 $.getArg 0 $.isNone then
+if stx[1][0].isNone then
  none
 else
-  some $ stx.getArg 1 $.getArg 0 $.getIdAt 0
+  some stx[1][0][0].getId

 private def getMajor (stx : Syntax) : Syntax :=
-stx.getArg 1 $.getArg 1
+stx[1][1]

 private def elabMajor (h? : Option Name) (major : Syntax) : TacticM Expr := do
 match h? with
@ -57,12 +57,12 @@ match major with
  `stx` is syntax for `induction`. -/
 private def getGeneralizingFVarIds (stx : Syntax) : TacticM (Array FVarId) :=
 withRef stx $
-let generalizingStx := stx.getArg 3
+let generalizingStx := stx[3]
 if generalizingStx.isNone then
  pure #[]
 else withMainMVarContext do
  trace `Elab.induction fun _ => generalizingStx
-  let vars := (generalizingStx.getArg 1).getArgs
+  let vars := generalizingStx[1].getArgs
  getFVarIds vars

 -- process `generalizingVars` subterm of induction Syntax `stx`.
@ -75,16 +75,16 @@ liftMetaTacticAux fun mvarId => do
  pure (fvarIds.size, [mvarId'])

 private def getAlts (withAlts : Syntax) : Array Syntax :=
-withAlts.getArg 2 $.getSepArgs
+withAlts[2].getSepArgs

 /-
  Given an `inductionAlt` of the form
  ```
  nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> termParser
  ``` -/
-private def getAltName (alt : Syntax) : Name := (alt.getArg 0).getId.eraseMacroScopes
-private def getAltVarNames (alt : Syntax) : Array Name := (alt.getArg 1).getArgs.map Syntax.getId
-private def getAltRHS (alt : Syntax) : Syntax := alt.getArg 3
+private def getAltName (alt : Syntax) : Name := alt[0].getId.eraseMacroScopes
+private def getAltVarNames (alt : Syntax) : Array Name := alt[1].getArgs.map Syntax.getId
+private def getAltRHS (alt : Syntax) : Syntax := alt[3]

 /-
  Given alts of the form
@ -98,7 +98,7 @@ for alt in alts do
  let n := getAltName alt
  withRef alt $ trace[Elab.checkAlt]! "{n} , {alt}"
  unless n == `_ || ctorNames.any (fun ctorName => n.isSuffixOf ctorName) do
-    throwErrorAt! (alt.getArg 0) "invalid constructor name '{n}'"
+    throwErrorAt! alt[0] "invalid constructor name '{n}'"

 structure RecInfo :=
 (recName : Name)
@ -199,8 +199,8 @@ else
  ``` -/
 private def getRecInfo (stx : Syntax) (major : Expr) : TacticM RecInfo :=
 withRef stx do
-let usingRecStx := stx.getArg 2
-let withAlts    := stx.getArg 4
+let usingRecStx := stx[2]
+let withAlts    := stx[4]
 if usingRecStx.isNone then
  let (rinfo, _) ← getRecInfoDefault major withAlts false
  pure rinfo
@ -317,7 +317,7 @@ fun stx => focusAux do
  let major ← elabMajor h? (getMajor stx)
  let major ← generalizeMajor major
  let (mvarId, _) ← getMainGoal
-  let withAlts := stx.getArg 2
+  let withAlts := stx[2]
  let (recInfo, ctorNames) ← getRecInfoDefault major withAlts true
  let result ← Meta.cases mvarId major.fvarId! recInfo.altVars
  checkCasesResult result ctorNames recInfo.altRHSs
--- a/stage0/src/Lean/Elab/Tactic/Injection.lean
+++ b/stage0/src/Lean/Elab/Tactic/Injection.lean
@ -11,7 +11,7 @@ namespace Lean.Elab.Tactic
 -- optional (" with " >> many1 ident')
 private def getInjectionNewIds (stx : Syntax) : List Name :=
 if stx.isNone then []
-else stx.getArg 1 $.getArgs.toList.map Syntax.getId
+else stx[1].getArgs.toList.map Syntax.getId

 private def checkUnusedIds (mvarId : MVarId) (unusedIds : List Name) : MetaM Unit := do
 unless unusedIds.isEmpty do
@ -20,8 +20,8 @@ unless unusedIds.isEmpty do
@[builtinTactic «injection»] def evalInjection : Tactic :=
 fun stx => do
  -- parser! nonReservedSymbol "injection " >> termParser >> withIds
-  let fvarId ← elabAsFVar (stx.getArg 1)
-  let ids := getInjectionNewIds (stx.getArg 2)
+  let fvarId ← elabAsFVar stx[1]
+  let ids := getInjectionNewIds stx[2]
  liftMetaTactic fun mvarId => do
    match ← Meta.injection mvarId fvarId ids (!ids.isEmpty) with
    | Meta.InjectionResult.solved                      => checkUnusedIds mvarId ids; pure []
--- a/stage0/src/Lean/Elab/Tactic/Location.lean
+++ b/stage0/src/Lean/Elab/Tactic/Location.lean
@ -21,13 +21,13 @@ def location         := parser! "at " >> (locationWildcard <|> locationTarget <|
 ```
 -/
 def expandLocation (stx : Syntax) : Location :=
-let arg := stx.getArg 1
+let arg := stx[1]
 if arg.getKind == `Lean.Parser.Tactic.locationWildcard then Location.wildcard
 else if arg.getKind == `Lean.Parser.Tactic.locationTarget then Location.target
-else Location.localDecls $ arg.getArg 0 $.getArgs.map fun stx => stx.getId
+else Location.localDecls $ arg[0].getArgs.map fun stx => stx.getId

 def expandOptLocation (stx : Syntax) : Location :=
 if stx.isNone then Location.target
-else expandLocation $ stx.getArg 0
+else expandLocation stx[0]

 end Lean.Elab.Tactic
--- a/stage0/src/Lean/Elab/Tactic/Match.lean
+++ b/stage0/src/Lean/Elab/Tactic/Match.lean
@ -15,11 +15,11 @@ structure AuxMatchTermState :=
 (cases   : Array Syntax := #[])

 private def mkAuxiliaryMatchTermAux (parentTag : Name) (matchTac : Syntax) : StateT AuxMatchTermState MacroM Syntax := do
-let matchAlts := matchTac.getArg 4
-let alts      := matchAlts.getArg 1 $.getArgs
+let matchAlts := matchTac[4]
+let alts      := matchAlts[1].getArgs
 let newAlts ← alts.mapSepElemsM fun alt => do
  let alt    := alt.updateKind `Lean.Parser.Term.matchAlt
-  let holeOrTacticSeq := alt.getArg 2
+  let holeOrTacticSeq := alt[2]
  if holeOrTacticSeq.isOfKind `Lean.Parser.Term.syntheticHole then
    pure alt
  else if holeOrTacticSeq.isOfKind `Lean.Parser.Term.hole then
@ -30,7 +30,7 @@ let newAlts ← alts.mapSepElemsM fun alt => do
    pure $ alt.setArg 2 newHole
  else withFreshMacroScope do
    let newHole ← `(?rhs)
-    let newHoleId := newHole.getArg 1
+    let newHoleId := newHole[1]
    let newCase ← `(tactic| case $newHoleId => $holeOrTacticSeq:tacticSeq )
    modify fun s => { s with cases := s.cases.push newCase }
    pure $ alt.setArg 2 newHole
--- a/stage0/src/Lean/Elab/Tactic/Rewrite.lean
+++ b/stage0/src/Lean/Elab/Tactic/Rewrite.lean
@ -14,8 +14,8 @@ open Meta

@[builtinMacro Lean.Parser.Tactic.rewriteSeq] def expandRewriteTactic : Macro :=
 fun stx =>
-  let seq := ((stx.getArg 1).getArg 1).getSepArgs
-  let loc := stx.getArg 2
+  let seq := stx[1][1].getSepArgs
+  let loc := stx[2]
  pure $ mkNullNode $ seq.map fun rwRule => Syntax.node `Lean.Parser.Tactic.rewrite #[mkAtomFrom rwRule "rewrite ", rwRule, loc]

 def rewriteTarget (stx : Syntax) (symm : Bool) : TacticM Unit := do
@ -59,10 +59,10 @@ def «rewrite» := parser! "rewrite" >> rwRule >> optional location
 -/
@[builtinTactic Lean.Parser.Tactic.rewrite] def evalRewrite : Tactic :=
 fun stx => do
-  let rule := stx.getArg 1
-  let symm := !(rule.getArg 0).isNone
-  let term := rule.getArg 1
-  let loc  := expandOptLocation $ stx.getArg 2
+  let rule := stx[1]
+  let symm := !rule[0].isNone
+  let term := rule[1]
+  let loc  := expandOptLocation stx[2]
  match loc with
  | Location.target => rewriteTarget term symm
  | Location.localDecls userNames => userNames.forM (rewriteLocalDecl term symm)
--- a/stage0/stdlib/Init/LeanInit.c
+++ b/stage0/stdlib/Init/LeanInit.c
@ -421,6 +421,7 @@ lean_object* l_Lean_mkStxLit(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_toNat(lean_object*);
 lean_object* l_Lean_mkOptionalNode___closed__2;
+lean_object* l_Lean_Syntax_getOp___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getOptional_x3f___boxed(lean_object*);
 lean_object* l_Lean_mkCIdentFrom___closed__2;
 lean_object* lean_nat_mod(lean_object*, lean_object*);
@ -464,6 +465,7 @@ lean_object* l___private_Init_LeanInit_3__assembleParts___main(lean_object*, lea
 lean_object* l_Lean_defaultMaxRecDepth;
 lean_object* l_Lean_Syntax_decodeStrLitAux(lean_object*, lean_object*, lean_object*);
 uint8_t lean_string_utf8_at_end(lean_object*, lean_object*);
+lean_object* l_Lean_Syntax_getOp(lean_object*, lean_object*);
 lean_object* lean_uint32_to_nat(uint32_t);
 lean_object* l___private_Init_LeanInit_9__decodeHexDigit___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_decodeStrLitAux___main(lean_object*, lean_object*, lean_object*);
@ -2157,6 +2159,24 @@ lean_dec(x_1);
 return x_3;
 }
 }
+lean_object* l_Lean_Syntax_getOp(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Lean_Syntax_getArg(x_1, x_2);
+return x_3;
+}
+}
+lean_object* l_Lean_Syntax_getOp___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Lean_Syntax_getOp(x_1, x_2);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_3;
+}
+}
 lean_object* l_Lean_Syntax_getArgs(lean_object* x_1) {
 _start:
 {
--- a/stage0/stdlib/Lean/Elab/Attributes.c
+++ b/stage0/stdlib/Lean/Elab/Attributes.c
@ -13,61 +13,90 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
-lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_elabAttrs___spec__1___rarg___lambda__1___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_Array_mapM___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+size_t l_USize_add(size_t, size_t);
+lean_object* l_Lean_stringToMessageData(lean_object*);
+lean_object* lean_array_uget(lean_object*, size_t);
 lean_object* l_Lean_Format_pretty(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Attribute_inhabited;
+lean_object* l_Lean_Elab_Attribute_args___default;
 lean_object* l_Lean_withRef___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Array_empty___closed__1;
-extern lean_object* l_Lean_MessageData_arrayExpr_toMessageData___main___closed__1;
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_elabAttr___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
-lean_object* l_Lean_Elab_elabAttr___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* lean_nat_add(lean_object*, lean_object*);
-lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_elabAttrs___spec__1___rarg___lambda__1(lean_object*, 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_elabAttr___rarg___lambda__8___boxed(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_Lean_Elab_elabAttrs___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
+extern lean_object* l_List_repr___rarg___closed__3;
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+uint8_t l_USize_decLt(size_t, size_t);
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_elabAttrs___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_elabAttrs___spec__1(lean_object*);
 lean_object* l_Lean_Elab_elabAttrs___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Attribute_hasFormat___closed__1;
 extern lean_object* l_Lean_Format_join___closed__1;
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_elabAttrs(lean_object*);
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__9(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_elabAttr(lean_object*);
+lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg___lambda__3(lean_object*, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
 lean_object* l_Lean_Elab_Attribute_hasFormat(lean_object*);
+lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1(lean_object*);
+lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Attribute_hasFormat___closed__2;
+size_t lean_usize_of_nat(lean_object*);
 lean_object* l_Lean_Elab_elabAttr___rarg___closed__2;
 lean_object* l_Lean_Elab_Attribute_hasFormat___closed__4;
 lean_object* l_Lean_Elab_elabAttr___rarg___closed__1;
 lean_object* l_Lean_Elab_elabDeclAttrs___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_elabAttr_match__1(lean_object*);
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Syntax_isMissing(lean_object*);
 lean_object* l_Lean_Syntax_isIdOrAtom_x3f(lean_object*);
 lean_object* l_Lean_Elab_elabAttr___rarg___closed__3;
 lean_object* l_Lean_Elab_elabDeclAttrs(lean_object*);
+lean_object* l_Lean_Syntax_getSepArgs(lean_object*);
 uint8_t l_Lean_isAttribute(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getNumArgs(lean_object*);
 lean_object* l_Lean_Elab_elabAttr___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_elabAttrs___rarg___lambda__1(lean_object*, lean_object*);
 extern lean_object* l_Lean_Format_sbracket___closed__4;
-lean_object* l_Lean_Syntax_getArgs(lean_object*);
 lean_object* l_Lean_Elab_Attribute_inhabited___closed__1;
-lean_object* l_Lean_Elab_elabAttr___rarg___lambda__2___closed__1;
-lean_object* l_Lean_Elab_elabAttr___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_elabAttr___rarg___lambda__2___closed__2;
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_throwError___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_elabAttrs___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_elabAttr___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_string_length(lean_object*);
+lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
-lean_object* l_Lean_Elab_elabAttr___rarg___lambda__2___closed__3;
 lean_object* l_Lean_Syntax_formatStxAux___main(lean_object*, uint8_t, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Attribute_hasFormat___closed__3;
 extern lean_object* l_System_FilePath_dirName___closed__1;
 lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
 lean_object* l_Lean_Elab_elabAttr___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__5___closed__2;
+lean_object* l_Lean_Elab_elabAttr_match__1___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__5___closed__3;
 lean_object* lean_nat_to_int(lean_object*);
-uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__5___closed__1;
 lean_object* l_Lean_Elab_elabDeclAttrs___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* _init_l_Lean_Elab_Attribute_args___default() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_box(0);
+return x_1;
+}
+}
 static lean_object* _init_l_Lean_Elab_Attribute_hasFormat___closed__1() {
 _start:
 {
@ -198,51 +227,143 @@ x_1 = l_Lean_Elab_Attribute_inhabited___closed__1;
 return x_1;
 }
 }
+lean_object* l_Lean_Elab_elabAttr_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_4; lean_object* x_5; 
+lean_dec(x_3);
+x_4 = lean_box(0);
+x_5 = lean_apply_1(x_2, x_4);
+return x_5;
+}
+else
+{
+lean_object* x_6; lean_object* x_7; 
+lean_dec(x_2);
+x_6 = lean_ctor_get(x_1, 0);
+lean_inc(x_6);
+lean_dec(x_1);
+x_7 = lean_apply_1(x_3, x_6);
+return x_7;
+}
+}
+}
+lean_object* l_Lean_Elab_elabAttr_match__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_Elab_elabAttr_match__1___rarg), 3, 0);
+return x_2;
+}
+}
 lean_object* l_Lean_Elab_elabAttr___rarg___lambda__1(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; 
-x_5 = lean_unsigned_to_nat(1u);
-x_6 = l_Lean_Syntax_getArg(x_1, x_5);
-x_7 = l_Lean_Syntax_getNumArgs(x_6);
-x_8 = lean_unsigned_to_nat(0u);
-x_9 = lean_nat_dec_eq(x_7, x_8);
-lean_dec(x_7);
-if (x_9 == 0)
+lean_object* x_5; lean_object* x_6; 
+x_5 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_5, 0, x_1);
+lean_ctor_set(x_5, 1, x_2);
+x_6 = lean_apply_2(x_3, lean_box(0), x_5);
+return x_6;
+}
+}
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
 {
-lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; 
-x_10 = lean_ctor_get(x_2, 0);
-lean_inc(x_10);
-lean_dec(x_2);
-x_11 = lean_ctor_get(x_10, 1);
+lean_object* x_4; lean_object* x_5; lean_object* x_6; 
+x_4 = lean_box(0);
+x_5 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_5, 0, x_1);
+lean_ctor_set(x_5, 1, x_4);
+x_6 = lean_apply_2(x_2, lean_box(0), x_5);
+return x_6;
+}
+}
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__3(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; 
+x_6 = lean_unsigned_to_nat(1u);
+x_7 = l_Lean_Syntax_getArg(x_1, x_6);
+x_8 = l_Lean_Syntax_getNumArgs(x_7);
+x_9 = lean_unsigned_to_nat(0u);
+x_10 = lean_nat_dec_eq(x_8, x_9);
+lean_dec(x_8);
+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; 
+x_11 = lean_ctor_get(x_2, 0);
 lean_inc(x_11);
-lean_dec(x_10);
-x_12 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_12, 0, x_3);
-lean_ctor_set(x_12, 1, x_6);
-x_13 = lean_apply_2(x_11, lean_box(0), x_12);
+lean_dec(x_2);
+x_12 = lean_ctor_get(x_11, 1);
+lean_inc(x_12);
+lean_dec(x_11);
+x_13 = lean_box(0);
+lean_inc(x_12);
+x_14 = lean_apply_2(x_12, lean_box(0), x_13);
+x_15 = lean_alloc_closure((void*)(l_Lean_Elab_elabAttr___rarg___lambda__1___boxed), 4, 3);
+lean_closure_set(x_15, 0, x_3);
+lean_closure_set(x_15, 1, x_7);
+lean_closure_set(x_15, 2, x_12);
+x_16 = lean_apply_4(x_4, lean_box(0), lean_box(0), x_14, x_15);
+return x_16;
+}
+else
+{
+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_dec(x_7);
+x_17 = lean_ctor_get(x_2, 0);
+lean_inc(x_17);
+lean_dec(x_2);
+x_18 = lean_ctor_get(x_17, 1);
+lean_inc(x_18);
+lean_dec(x_17);
+x_19 = lean_box(0);
+lean_inc(x_18);
+x_20 = lean_apply_2(x_18, lean_box(0), x_19);
+x_21 = lean_alloc_closure((void*)(l_Lean_Elab_elabAttr___rarg___lambda__2___boxed), 3, 2);
+lean_closure_set(x_21, 0, x_3);
+lean_closure_set(x_21, 1, x_18);
+x_22 = lean_apply_4(x_4, lean_box(0), lean_box(0), x_20, x_21);
+return x_22;
+}
+}
+}
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; 
+x_7 = lean_unsigned_to_nat(1u);
+x_8 = l_Lean_Syntax_getArg(x_1, x_7);
+x_9 = l_Lean_Syntax_getNumArgs(x_8);
+x_10 = lean_unsigned_to_nat(0u);
+x_11 = lean_nat_dec_eq(x_9, x_10);
+lean_dec(x_9);
+if (x_11 == 0)
+{
+lean_object* x_12; lean_object* x_13; 
+x_12 = lean_alloc_closure((void*)(l_Lean_Elab_elabAttr___rarg___lambda__1___boxed), 4, 3);
+lean_closure_set(x_12, 0, x_2);
+lean_closure_set(x_12, 1, x_8);
+lean_closure_set(x_12, 2, x_3);
+x_13 = lean_apply_4(x_4, lean_box(0), lean_box(0), x_5, x_12);
 return x_13;
 }
 else
 {
-lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; 
-lean_dec(x_6);
-x_14 = lean_ctor_get(x_2, 0);
-lean_inc(x_14);
-lean_dec(x_2);
-x_15 = lean_ctor_get(x_14, 1);
-lean_inc(x_15);
-lean_dec(x_14);
-x_16 = lean_box(0);
-x_17 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_17, 0, x_3);
-lean_ctor_set(x_17, 1, x_16);
-x_18 = lean_apply_2(x_15, lean_box(0), x_17);
-return x_18;
+lean_object* x_14; lean_object* x_15; 
+lean_dec(x_8);
+x_14 = lean_alloc_closure((void*)(l_Lean_Elab_elabAttr___rarg___lambda__2___boxed), 3, 2);
+lean_closure_set(x_14, 0, x_2);
+lean_closure_set(x_14, 1, x_3);
+x_15 = lean_apply_4(x_4, lean_box(0), lean_box(0), x_5, x_14);
+return x_15;
 }
 }
 }
-static lean_object* _init_l_Lean_Elab_elabAttr___rarg___lambda__2___closed__1() {
+static lean_object* _init_l_Lean_Elab_elabAttr___rarg___lambda__5___closed__1() {
 _start:
 {
 lean_object* x_1; 
@ -250,75 +371,83 @@ x_1 = lean_mk_string("unknown attribute [");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Elab_elabAttr___rarg___lambda__2___closed__2() {
+static lean_object* _init_l_Lean_Elab_elabAttr___rarg___lambda__5___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Elab_elabAttr___rarg___lambda__2___closed__1;
-x_2 = lean_alloc_ctor(2, 1, 0);
-lean_ctor_set(x_2, 0, x_1);
+x_1 = l_Lean_Elab_elabAttr___rarg___lambda__5___closed__1;
+x_2 = l_Lean_stringToMessageData(x_1);
 return x_2;
 }
 }
-static lean_object* _init_l_Lean_Elab_elabAttr___rarg___lambda__2___closed__3() {
+static lean_object* _init_l_Lean_Elab_elabAttr___rarg___lambda__5___closed__3() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Elab_elabAttr___rarg___lambda__2___closed__2;
-x_2 = lean_alloc_ctor(0, 1, 0);
-lean_ctor_set(x_2, 0, x_1);
+x_1 = l_List_repr___rarg___closed__3;
+x_2 = l_Lean_stringToMessageData(x_1);
 return x_2;
 }
 }
-lean_object* l_Lean_Elab_elabAttr___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__5(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
 _start:
 {
-uint8_t x_9; lean_object* x_10; 
+uint8_t x_9; 
 x_9 = l_Lean_isAttribute(x_8, x_1);
-lean_inc(x_1);
-lean_inc(x_3);
-x_10 = lean_alloc_closure((void*)(l_Lean_Elab_elabAttr___rarg___lambda__1___boxed), 4, 3);
-lean_closure_set(x_10, 0, x_2);
-lean_closure_set(x_10, 1, x_3);
-lean_closure_set(x_10, 2, x_1);
 if (x_9 == 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; 
-x_11 = lean_alloc_ctor(4, 1, 0);
-lean_ctor_set(x_11, 0, x_1);
-x_12 = l_Lean_Elab_elabAttr___rarg___lambda__2___closed__3;
-x_13 = lean_alloc_ctor(10, 2, 0);
-lean_ctor_set(x_13, 0, x_12);
-lean_ctor_set(x_13, 1, x_11);
-x_14 = l_Lean_MessageData_arrayExpr_toMessageData___main___closed__1;
-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___rarg(x_3, x_4, x_5, x_6, lean_box(0), x_15);
-x_17 = lean_apply_4(x_7, lean_box(0), lean_box(0), x_16, x_10);
+lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; 
+lean_inc(x_1);
+x_10 = lean_alloc_ctor(4, 1, 0);
+lean_ctor_set(x_10, 0, x_1);
+x_11 = l_Lean_Elab_elabAttr___rarg___lambda__5___closed__2;
+x_12 = lean_alloc_ctor(10, 2, 0);
+lean_ctor_set(x_12, 0, x_11);
+lean_ctor_set(x_12, 1, x_10);
+x_13 = l_Lean_Elab_elabAttr___rarg___lambda__5___closed__3;
+x_14 = lean_alloc_ctor(10, 2, 0);
+lean_ctor_set(x_14, 0, x_12);
+lean_ctor_set(x_14, 1, x_13);
+lean_inc(x_2);
+x_15 = l_Lean_throwError___rarg(x_2, x_3, x_4, x_5, lean_box(0), x_14);
+lean_inc(x_7);
+x_16 = lean_alloc_closure((void*)(l_Lean_Elab_elabAttr___rarg___lambda__3___boxed), 5, 4);
+lean_closure_set(x_16, 0, x_6);
+lean_closure_set(x_16, 1, x_2);
+lean_closure_set(x_16, 2, x_1);
+lean_closure_set(x_16, 3, x_7);
+x_17 = lean_apply_4(x_7, lean_box(0), lean_box(0), x_15, x_16);
 return x_17;
 }
 else
 {
-lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; 
-lean_dec(x_6);
+lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; 
 lean_dec(x_5);
 lean_dec(x_4);
-lean_dec(x_1);
-x_18 = lean_ctor_get(x_3, 0);
-lean_inc(x_18);
 lean_dec(x_3);
+x_18 = lean_ctor_get(x_2, 0);
+lean_inc(x_18);
+lean_dec(x_2);
 x_19 = lean_ctor_get(x_18, 1);
 lean_inc(x_19);
 lean_dec(x_18);
 x_20 = lean_box(0);
+lean_inc(x_19);
 x_21 = lean_apply_2(x_19, lean_box(0), x_20);
-x_22 = lean_apply_4(x_7, lean_box(0), lean_box(0), x_21, x_10);
-return x_22;
+lean_inc(x_21);
+lean_inc(x_7);
+x_22 = lean_alloc_closure((void*)(l_Lean_Elab_elabAttr___rarg___lambda__4___boxed), 6, 5);
+lean_closure_set(x_22, 0, x_6);
+lean_closure_set(x_22, 1, x_1);
+lean_closure_set(x_22, 2, x_19);
+lean_closure_set(x_22, 3, x_7);
+lean_closure_set(x_22, 4, x_21);
+x_23 = lean_apply_4(x_7, lean_box(0), lean_box(0), x_21, x_22);
+return x_23;
 }
 }
 }
-lean_object* l_Lean_Elab_elabAttr___rarg___lambda__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* l_Lean_Elab_elabAttr___rarg___lambda__6(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; 
@ -326,7 +455,7 @@ x_9 = lean_ctor_get(x_1, 0);
 lean_inc(x_9);
 lean_dec(x_1);
 lean_inc(x_7);
-x_10 = lean_alloc_closure((void*)(l_Lean_Elab_elabAttr___rarg___lambda__2___boxed), 8, 7);
+x_10 = lean_alloc_closure((void*)(l_Lean_Elab_elabAttr___rarg___lambda__5___boxed), 8, 7);
 lean_closure_set(x_10, 0, x_8);
 lean_closure_set(x_10, 1, x_2);
 lean_closure_set(x_10, 2, x_3);
@ -338,6 +467,117 @@ x_11 = lean_apply_4(x_7, lean_box(0), lean_box(0), x_9, x_10);
 return x_11;
 }
 }
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__7(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; 
+x_6 = lean_unsigned_to_nat(1u);
+x_7 = l_Lean_Syntax_getArg(x_1, x_6);
+x_8 = l_Lean_Syntax_getNumArgs(x_7);
+x_9 = lean_unsigned_to_nat(0u);
+x_10 = lean_nat_dec_eq(x_8, x_9);
+lean_dec(x_8);
+if (x_10 == 0)
+{
+lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; 
+x_11 = lean_box(0);
+lean_inc(x_2);
+x_12 = lean_apply_2(x_2, lean_box(0), x_11);
+x_13 = lean_alloc_closure((void*)(l_Lean_Elab_elabAttr___rarg___lambda__1___boxed), 4, 3);
+lean_closure_set(x_13, 0, x_3);
+lean_closure_set(x_13, 1, x_7);
+lean_closure_set(x_13, 2, x_2);
+x_14 = lean_apply_4(x_4, lean_box(0), lean_box(0), x_12, x_13);
+return x_14;
+}
+else
+{
+lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; 
+lean_dec(x_7);
+x_15 = lean_box(0);
+lean_inc(x_2);
+x_16 = lean_apply_2(x_2, lean_box(0), x_15);
+x_17 = lean_alloc_closure((void*)(l_Lean_Elab_elabAttr___rarg___lambda__2___boxed), 3, 2);
+lean_closure_set(x_17, 0, x_3);
+lean_closure_set(x_17, 1, x_2);
+x_18 = lean_apply_4(x_4, lean_box(0), lean_box(0), x_16, x_17);
+return x_18;
+}
+}
+}
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__8(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) {
+_start:
+{
+uint8_t x_10; 
+x_10 = l_Lean_isAttribute(x_9, x_1);
+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; lean_object* x_18; 
+lean_inc(x_1);
+x_11 = lean_alloc_ctor(4, 1, 0);
+lean_ctor_set(x_11, 0, x_1);
+x_12 = l_Lean_Elab_elabAttr___rarg___lambda__5___closed__2;
+x_13 = lean_alloc_ctor(10, 2, 0);
+lean_ctor_set(x_13, 0, x_12);
+lean_ctor_set(x_13, 1, x_11);
+x_14 = l_Lean_Elab_elabAttr___rarg___lambda__5___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___rarg(x_2, x_3, x_4, x_5, lean_box(0), x_15);
+lean_inc(x_8);
+x_17 = lean_alloc_closure((void*)(l_Lean_Elab_elabAttr___rarg___lambda__7___boxed), 5, 4);
+lean_closure_set(x_17, 0, x_6);
+lean_closure_set(x_17, 1, x_7);
+lean_closure_set(x_17, 2, x_1);
+lean_closure_set(x_17, 3, x_8);
+x_18 = lean_apply_4(x_8, lean_box(0), lean_box(0), x_16, x_17);
+return x_18;
+}
+else
+{
+lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; 
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+x_19 = lean_box(0);
+lean_inc(x_7);
+x_20 = lean_apply_2(x_7, lean_box(0), x_19);
+lean_inc(x_20);
+lean_inc(x_8);
+x_21 = lean_alloc_closure((void*)(l_Lean_Elab_elabAttr___rarg___lambda__4___boxed), 6, 5);
+lean_closure_set(x_21, 0, x_6);
+lean_closure_set(x_21, 1, x_1);
+lean_closure_set(x_21, 2, x_7);
+lean_closure_set(x_21, 3, x_8);
+lean_closure_set(x_21, 4, x_20);
+x_22 = lean_apply_4(x_8, lean_box(0), lean_box(0), x_20, x_21);
+return x_22;
+}
+}
+}
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__9(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) {
+_start:
+{
+lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+x_10 = lean_ctor_get(x_1, 0);
+lean_inc(x_10);
+lean_dec(x_1);
+lean_inc(x_8);
+x_11 = lean_alloc_closure((void*)(l_Lean_Elab_elabAttr___rarg___lambda__8___boxed), 9, 8);
+lean_closure_set(x_11, 0, x_9);
+lean_closure_set(x_11, 1, x_2);
+lean_closure_set(x_11, 2, x_3);
+lean_closure_set(x_11, 3, x_4);
+lean_closure_set(x_11, 4, x_5);
+lean_closure_set(x_11, 5, x_6);
+lean_closure_set(x_11, 6, x_7);
+lean_closure_set(x_11, 7, x_8);
+x_12 = lean_apply_4(x_8, lean_box(0), lean_box(0), x_10, x_11);
+return x_12;
+}
+}
 static lean_object* _init_l_Lean_Elab_elabAttr___rarg___closed__1() {
 _start:
 {
@ -369,63 +609,72 @@ return x_2;
 lean_object* l_Lean_Elab_elabAttr___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
 _start:
 {
-lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+lean_object* x_7; lean_object* x_8; lean_object* x_9; 
 x_7 = lean_unsigned_to_nat(0u);
 x_8 = l_Lean_Syntax_getArg(x_6, x_7);
-x_9 = lean_ctor_get(x_1, 1);
-lean_inc(x_9);
-x_10 = l_Lean_Syntax_isIdOrAtom_x3f(x_8);
-lean_inc(x_9);
+x_9 = l_Lean_Syntax_isIdOrAtom_x3f(x_8);
+if (lean_obj_tag(x_9) == 0)
+{
+lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; 
+x_10 = lean_ctor_get(x_1, 1);
+lean_inc(x_10);
+x_11 = l_Lean_Elab_elabAttr___rarg___closed__3;
 lean_inc(x_5);
 lean_inc(x_4);
 lean_inc(x_3);
 lean_inc(x_1);
-x_11 = lean_alloc_closure((void*)(l_Lean_Elab_elabAttr___rarg___lambda__3), 8, 7);
-lean_closure_set(x_11, 0, x_2);
-lean_closure_set(x_11, 1, x_6);
-lean_closure_set(x_11, 2, x_1);
-lean_closure_set(x_11, 3, x_3);
-lean_closure_set(x_11, 4, x_4);
-lean_closure_set(x_11, 5, x_5);
-lean_closure_set(x_11, 6, x_9);
-if (lean_obj_tag(x_10) == 0)
-{
-lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; 
-x_12 = l_Lean_Elab_elabAttr___rarg___closed__3;
+x_12 = l_Lean_throwError___rarg(x_1, x_3, x_4, x_5, lean_box(0), x_11);
+x_13 = lean_ctor_get(x_4, 0);
+lean_inc(x_13);
 lean_inc(x_4);
-x_13 = l_Lean_throwError___rarg(x_1, x_3, x_4, x_5, lean_box(0), x_12);
-x_14 = lean_ctor_get(x_4, 0);
-lean_inc(x_14);
-x_15 = lean_alloc_closure((void*)(l_Lean_withRef___rarg___lambda__1___boxed), 4, 3);
-lean_closure_set(x_15, 0, x_8);
-lean_closure_set(x_15, 1, x_4);
-lean_closure_set(x_15, 2, x_13);
-lean_inc(x_9);
-x_16 = lean_apply_4(x_9, lean_box(0), lean_box(0), x_14, x_15);
-x_17 = lean_apply_4(x_9, lean_box(0), lean_box(0), x_16, x_11);
+x_14 = lean_alloc_closure((void*)(l_Lean_withRef___rarg___lambda__1___boxed), 4, 3);
+lean_closure_set(x_14, 0, x_8);
+lean_closure_set(x_14, 1, x_4);
+lean_closure_set(x_14, 2, x_12);
+lean_inc(x_10);
+x_15 = lean_apply_4(x_10, lean_box(0), lean_box(0), x_13, x_14);
+lean_inc(x_10);
+x_16 = lean_alloc_closure((void*)(l_Lean_Elab_elabAttr___rarg___lambda__6), 8, 7);
+lean_closure_set(x_16, 0, x_2);
+lean_closure_set(x_16, 1, x_1);
+lean_closure_set(x_16, 2, x_3);
+lean_closure_set(x_16, 3, x_4);
+lean_closure_set(x_16, 4, x_5);
+lean_closure_set(x_16, 5, x_6);
+lean_closure_set(x_16, 6, x_10);
+x_17 = lean_apply_4(x_10, lean_box(0), lean_box(0), x_15, x_16);
 return x_17;
 }
 else
 {
-lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; 
+lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; 
 lean_dec(x_8);
-lean_dec(x_5);
-lean_dec(x_4);
-lean_dec(x_3);
-x_18 = lean_ctor_get(x_10, 0);
+x_18 = lean_ctor_get(x_9, 0);
 lean_inc(x_18);
-lean_dec(x_10);
-x_19 = lean_ctor_get(x_1, 0);
+lean_dec(x_9);
+x_19 = lean_ctor_get(x_1, 1);
 lean_inc(x_19);
-lean_dec(x_1);
-x_20 = lean_ctor_get(x_19, 1);
+x_20 = lean_ctor_get(x_1, 0);
 lean_inc(x_20);
-lean_dec(x_19);
-x_21 = lean_box(0);
-x_22 = lean_name_mk_string(x_21, x_18);
-x_23 = lean_apply_2(x_20, lean_box(0), x_22);
-x_24 = lean_apply_4(x_9, lean_box(0), lean_box(0), x_23, x_11);
-return x_24;
+x_21 = lean_ctor_get(x_20, 1);
+lean_inc(x_21);
+lean_dec(x_20);
+x_22 = lean_box(0);
+x_23 = lean_name_mk_string(x_22, x_18);
+lean_inc(x_21);
+x_24 = lean_apply_2(x_21, lean_box(0), x_23);
+lean_inc(x_19);
+x_25 = lean_alloc_closure((void*)(l_Lean_Elab_elabAttr___rarg___lambda__9), 9, 8);
+lean_closure_set(x_25, 0, x_2);
+lean_closure_set(x_25, 1, x_1);
+lean_closure_set(x_25, 2, x_3);
+lean_closure_set(x_25, 3, x_4);
+lean_closure_set(x_25, 4, x_5);
+lean_closure_set(x_25, 5, x_6);
+lean_closure_set(x_25, 6, x_21);
+lean_closure_set(x_25, 7, x_19);
+x_26 = lean_apply_4(x_19, lean_box(0), lean_box(0), x_24, x_25);
+return x_26;
 }
 }
 }
@ -443,39 +692,142 @@ _start:
 lean_object* x_5; 
 x_5 = l_Lean_Elab_elabAttr___rarg___lambda__1(x_1, x_2, x_3, x_4);
 lean_dec(x_4);
-lean_dec(x_1);
 return x_5;
 }
 }
-lean_object* l_Lean_Elab_elabAttr___rarg___lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = l_Lean_Elab_elabAttr___rarg___lambda__2(x_1, x_2, x_3);
+lean_dec(x_3);
+return x_4;
+}
+}
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__3___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_Elab_elabAttr___rarg___lambda__3(x_1, x_2, x_3, x_4, x_5);
+lean_dec(x_5);
+lean_dec(x_1);
+return x_6;
+}
+}
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__4___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_elabAttr___rarg___lambda__4(x_1, x_2, x_3, x_4, x_5, x_6);
+lean_dec(x_6);
+lean_dec(x_1);
+return x_7;
+}
+}
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__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, lean_object* x_8) {
 _start:
 {
 lean_object* x_9; 
-x_9 = l_Lean_Elab_elabAttr___rarg___lambda__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
+x_9 = l_Lean_Elab_elabAttr___rarg___lambda__5(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
 lean_dec(x_8);
 return x_9;
 }
 }
-lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_elabAttrs___spec__1___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__7___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_10; lean_object* x_11; 
-x_10 = lean_nat_add(x_1, x_2);
-x_11 = l_Array_foldlStepMAux___main___at_Lean_Elab_elabAttrs___spec__1___rarg(x_3, x_4, x_5, x_6, x_7, x_2, x_8, x_10, x_9);
+lean_object* x_6; 
+x_6 = l_Lean_Elab_elabAttr___rarg___lambda__7(x_1, x_2, x_3, x_4, x_5);
+lean_dec(x_5);
+lean_dec(x_1);
+return x_6;
+}
+}
+lean_object* l_Lean_Elab_elabAttr___rarg___lambda__8___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) {
+_start:
+{
+lean_object* x_10; 
+x_10 = l_Lean_Elab_elabAttr___rarg___lambda__8(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
+lean_dec(x_9);
+return x_10;
+}
+}
+lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; lean_object* x_5; 
+x_4 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_4, 0, x_1);
+x_5 = lean_apply_2(x_2, lean_box(0), x_4);
+return x_5;
+}
+}
+lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+x_5 = lean_array_push(x_1, x_4);
+x_6 = lean_ctor_get(x_2, 0);
+lean_inc(x_6);
+lean_dec(x_2);
+x_7 = lean_ctor_get(x_6, 1);
+lean_inc(x_7);
+lean_dec(x_6);
+x_8 = lean_box(0);
+lean_inc(x_7);
+x_9 = lean_apply_2(x_7, lean_box(0), x_8);
+x_10 = lean_alloc_closure((void*)(l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg___lambda__1___boxed), 3, 2);
+lean_closure_set(x_10, 0, x_5);
+lean_closure_set(x_10, 1, x_7);
+x_11 = lean_apply_4(x_3, lean_box(0), lean_box(0), x_9, x_10);
 return x_11;
 }
 }
-lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_elabAttrs___spec__1___rarg(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* l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg___lambda__3(lean_object* x_1, size_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, size_t x_9, lean_object* x_10) {
 _start:
 {
-lean_object* x_10; uint8_t x_11; 
-x_10 = lean_array_get_size(x_7);
-x_11 = lean_nat_dec_lt(x_8, x_10);
+if (lean_obj_tag(x_10) == 0)
+{
+lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; 
+lean_dec(x_8);
+lean_dec(x_7);
+lean_dec(x_6);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+x_11 = lean_ctor_get(x_10, 0);
+lean_inc(x_11);
 lean_dec(x_10);
+x_12 = lean_ctor_get(x_1, 0);
+lean_inc(x_12);
+lean_dec(x_1);
+x_13 = lean_ctor_get(x_12, 1);
+lean_inc(x_13);
+lean_dec(x_12);
+x_14 = lean_apply_2(x_13, lean_box(0), x_11);
+return x_14;
+}
+else
+{
+lean_object* x_15; size_t x_16; size_t x_17; lean_object* x_18; 
+x_15 = lean_ctor_get(x_10, 0);
+lean_inc(x_15);
+lean_dec(x_10);
+x_16 = 1;
+x_17 = x_2 + x_16;
+x_18 = l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg(x_1, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_17, x_15);
+return x_18;
+}
+}
+}
+lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg(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, size_t x_8, size_t x_9, lean_object* x_10) {
+_start:
+{
+uint8_t x_11; 
+x_11 = x_9 < x_8;
 if (x_11 == 0)
 {
 lean_object* x_12; lean_object* x_13; lean_object* x_14; 
-lean_dec(x_8);
 lean_dec(x_7);
 lean_dec(x_6);
 lean_dec(x_5);
@ -488,13 +840,13 @@ lean_dec(x_1);
 x_13 = lean_ctor_get(x_12, 1);
 lean_inc(x_13);
 lean_dec(x_12);
-x_14 = lean_apply_2(x_13, lean_box(0), x_9);
+x_14 = lean_apply_2(x_13, lean_box(0), x_10);
 return x_14;
 }
 else
 {
-lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; 
-x_15 = lean_array_fget(x_7, x_8);
+lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; 
+x_15 = lean_array_uget(x_7, x_9);
 x_16 = lean_ctor_get(x_1, 1);
 lean_inc(x_16);
 lean_inc(x_5);
@ -503,44 +855,72 @@ lean_inc(x_3);
 lean_inc(x_2);
 lean_inc(x_1);
 x_17 = l_Lean_Elab_elabAttr___rarg(x_1, x_2, x_3, x_4, x_5, x_15);
+lean_inc(x_6);
 lean_inc(x_1);
-x_18 = lean_alloc_closure((void*)(l_Array_iterateMAux___main___at_Array_mapM___spec__1___rarg___lambda__1), 3, 2);
-lean_closure_set(x_18, 0, x_1);
-lean_closure_set(x_18, 1, x_9);
-lean_inc(x_16);
-x_19 = lean_apply_4(x_16, lean_box(0), lean_box(0), x_17, x_18);
-x_20 = lean_alloc_closure((void*)(l_Array_foldlStepMAux___main___at_Lean_Elab_elabAttrs___spec__1___rarg___lambda__1___boxed), 9, 8);
-lean_closure_set(x_20, 0, x_8);
-lean_closure_set(x_20, 1, x_6);
-lean_closure_set(x_20, 2, x_1);
-lean_closure_set(x_20, 3, x_2);
-lean_closure_set(x_20, 4, x_3);
-lean_closure_set(x_20, 5, x_4);
-lean_closure_set(x_20, 6, x_5);
-lean_closure_set(x_20, 7, x_7);
-x_21 = lean_apply_4(x_16, lean_box(0), lean_box(0), x_19, x_20);
-return x_21;
+x_18 = lean_alloc_closure((void*)(l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg___lambda__2), 4, 3);
+lean_closure_set(x_18, 0, x_10);
+lean_closure_set(x_18, 1, x_1);
+lean_closure_set(x_18, 2, x_6);
+lean_inc(x_6);
+x_19 = lean_apply_4(x_6, lean_box(0), lean_box(0), x_17, x_18);
+x_20 = lean_box_usize(x_9);
+x_21 = lean_box_usize(x_8);
+x_22 = lean_alloc_closure((void*)(l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg___lambda__3___boxed), 10, 9);
+lean_closure_set(x_22, 0, x_1);
+lean_closure_set(x_22, 1, x_20);
+lean_closure_set(x_22, 2, x_2);
+lean_closure_set(x_22, 3, x_3);
+lean_closure_set(x_22, 4, x_4);
+lean_closure_set(x_22, 5, x_5);
+lean_closure_set(x_22, 6, x_6);
+lean_closure_set(x_22, 7, x_7);
+lean_closure_set(x_22, 8, x_21);
+x_23 = lean_apply_4(x_16, lean_box(0), lean_box(0), x_19, x_22);
+return x_23;
 }
 }
 }
-lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_elabAttrs___spec__1(lean_object* x_1) {
+lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_Array_foldlStepMAux___main___at_Lean_Elab_elabAttrs___spec__1___rarg), 9, 0);
+x_2 = lean_alloc_closure((void*)(l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg___boxed), 10, 0);
 return x_2;
 }
 }
+lean_object* l_Lean_Elab_elabAttrs___rarg___lambda__1(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_3 = lean_ctor_get(x_1, 0);
+lean_inc(x_3);
+lean_dec(x_1);
+x_4 = lean_ctor_get(x_3, 1);
+lean_inc(x_4);
+lean_dec(x_3);
+x_5 = lean_apply_2(x_4, lean_box(0), x_2);
+return x_5;
+}
+}
 lean_object* l_Lean_Elab_elabAttrs___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
 _start:
 {
-lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
-x_7 = l_Lean_Syntax_getArgs(x_6);
-x_8 = lean_unsigned_to_nat(2u);
-x_9 = lean_unsigned_to_nat(0u);
-x_10 = l_Array_empty___closed__1;
-x_11 = l_Array_foldlStepMAux___main___at_Lean_Elab_elabAttrs___spec__1___rarg(x_1, x_2, x_3, x_4, x_5, x_8, x_7, x_9, x_10);
-return x_11;
+lean_object* x_7; lean_object* x_8; lean_object* x_9; size_t x_10; size_t x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
+x_7 = lean_ctor_get(x_1, 1);
+lean_inc(x_7);
+x_8 = l_Lean_Syntax_getSepArgs(x_6);
+x_9 = lean_array_get_size(x_8);
+x_10 = lean_usize_of_nat(x_9);
+lean_dec(x_9);
+x_11 = 0;
+x_12 = l_Array_empty___closed__1;
+lean_inc(x_7);
+lean_inc(x_1);
+x_13 = l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg(x_1, x_2, x_3, x_4, x_5, x_7, x_8, x_10, x_11, x_12);
+x_14 = lean_alloc_closure((void*)(l_Lean_Elab_elabAttrs___rarg___lambda__1), 2, 1);
+lean_closure_set(x_14, 0, x_1);
+x_15 = lean_apply_4(x_7, lean_box(0), lean_box(0), x_13, x_14);
+return x_15;
 }
 }
 lean_object* l_Lean_Elab_elabAttrs(lean_object* x_1) {
@ -551,13 +931,37 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Elab_elabAttrs___rarg___boxed), 6, 0);
 return x_2;
 }
 }
-lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_elabAttrs___spec__1___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
+lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
-lean_object* x_10; 
-x_10 = l_Array_foldlStepMAux___main___at_Lean_Elab_elabAttrs___spec__1___rarg___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
-lean_dec(x_1);
-return x_10;
+lean_object* x_4; 
+x_4 = l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg___lambda__1(x_1, x_2, x_3);
+lean_dec(x_3);
+return x_4;
+}
+}
+lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg___lambda__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) {
+_start:
+{
+size_t x_11; size_t x_12; lean_object* x_13; 
+x_11 = lean_unbox_usize(x_2);
+lean_dec(x_2);
+x_12 = lean_unbox_usize(x_9);
+lean_dec(x_9);
+x_13 = l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg___lambda__3(x_1, x_11, x_3, x_4, x_5, x_6, x_7, x_8, x_12, x_10);
+return x_13;
+}
+}
+lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg___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) {
+_start:
+{
+size_t x_11; size_t x_12; lean_object* x_13; 
+x_11 = lean_unbox_usize(x_8);
+lean_dec(x_8);
+x_12 = lean_unbox_usize(x_9);
+lean_dec(x_9);
+x_13 = l_Array_forInUnsafe_loop___at_Lean_Elab_elabAttrs___spec__1___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_11, x_12, x_10);
+return x_13;
 }
 }
 lean_object* l_Lean_Elab_elabAttrs___rarg___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) {
@ -618,6 +1022,8 @@ lean_dec_ref(res);
 res = initialize_Lean_MonadEnv(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+l_Lean_Elab_Attribute_args___default = _init_l_Lean_Elab_Attribute_args___default();
+lean_mark_persistent(l_Lean_Elab_Attribute_args___default);
 l_Lean_Elab_Attribute_hasFormat___closed__1 = _init_l_Lean_Elab_Attribute_hasFormat___closed__1();
 lean_mark_persistent(l_Lean_Elab_Attribute_hasFormat___closed__1);
 l_Lean_Elab_Attribute_hasFormat___closed__2 = _init_l_Lean_Elab_Attribute_hasFormat___closed__2();
@ -630,12 +1036,12 @@ l_Lean_Elab_Attribute_inhabited___closed__1 = _init_l_Lean_Elab_Attribute_inhabi
 lean_mark_persistent(l_Lean_Elab_Attribute_inhabited___closed__1);
 l_Lean_Elab_Attribute_inhabited = _init_l_Lean_Elab_Attribute_inhabited();
 lean_mark_persistent(l_Lean_Elab_Attribute_inhabited);
-l_Lean_Elab_elabAttr___rarg___lambda__2___closed__1 = _init_l_Lean_Elab_elabAttr___rarg___lambda__2___closed__1();
-lean_mark_persistent(l_Lean_Elab_elabAttr___rarg___lambda__2___closed__1);
-l_Lean_Elab_elabAttr___rarg___lambda__2___closed__2 = _init_l_Lean_Elab_elabAttr___rarg___lambda__2___closed__2();
-lean_mark_persistent(l_Lean_Elab_elabAttr___rarg___lambda__2___closed__2);
-l_Lean_Elab_elabAttr___rarg___lambda__2___closed__3 = _init_l_Lean_Elab_elabAttr___rarg___lambda__2___closed__3();
-lean_mark_persistent(l_Lean_Elab_elabAttr___rarg___lambda__2___closed__3);
+l_Lean_Elab_elabAttr___rarg___lambda__5___closed__1 = _init_l_Lean_Elab_elabAttr___rarg___lambda__5___closed__1();
+lean_mark_persistent(l_Lean_Elab_elabAttr___rarg___lambda__5___closed__1);
+l_Lean_Elab_elabAttr___rarg___lambda__5___closed__2 = _init_l_Lean_Elab_elabAttr___rarg___lambda__5___closed__2();
+lean_mark_persistent(l_Lean_Elab_elabAttr___rarg___lambda__5___closed__2);
+l_Lean_Elab_elabAttr___rarg___lambda__5___closed__3 = _init_l_Lean_Elab_elabAttr___rarg___lambda__5___closed__3();
+lean_mark_persistent(l_Lean_Elab_elabAttr___rarg___lambda__5___closed__3);
 l_Lean_Elab_elabAttr___rarg___closed__1 = _init_l_Lean_Elab_elabAttr___rarg___closed__1();
 lean_mark_persistent(l_Lean_Elab_elabAttr___rarg___closed__1);
 l_Lean_Elab_elabAttr___rarg___closed__2 = _init_l_Lean_Elab_elabAttr___rarg___closed__2();
--- a/stage0/stdlib/Lean/Elab/DeclUtil.c
+++ b/stage0/stdlib/Lean/Elab/DeclUtil.c
--- a/stage0/stdlib/Lean/Elab/Declaration.c
+++ b/stage0/stdlib/Lean/Elab/Declaration.c
--- a/stage0/stdlib/Lean/Elab/Import.c
+++ b/stage0/stdlib/Lean/Elab/Import.c
@ -13,43 +13,48 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
+lean_object* lean_string_push(lean_object*, uint32_t);
 lean_object* l_Lean_Parser_parseHeader(lean_object*, lean_object*);
 lean_object* lean_io_error_to_string(lean_object*);
 lean_object* l_List_map___main___at_Lean_Elab_headerToImports___spec__1(lean_object*);
-lean_object* l_Lean_Syntax_getIdAt(lean_object*, lean_object*);
 lean_object* l_List_append___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_headerToImports___closed__2;
 lean_object* l_Lean_Elab_headerToImports(lean_object*);
+lean_object* l_List_forInAux___main___at_Lean_Elab_printDeps___spec__4___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_mkInputContext(lean_object*, lean_object*);
+lean_object* l_Lean_Elab_parseImports_match__1(lean_object*);
 extern lean_object* l_String_splitAux___main___closed__1;
+lean_object* l_IO_println___at_Lean_Elab_printDeps___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_headerToImports___closed__1;
 lean_object* l_Lean_Elab_headerToImports___boxed(lean_object*);
 lean_object* l_Lean_findOLean(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_processHeader(lean_object*, lean_object*, lean_object*, uint32_t, lean_object*);
 lean_object* l_Lean_Elab_parseImports___closed__1;
 lean_object* l_Lean_MessageLog_toList(lean_object*);
+lean_object* l_Lean_Elab_parseImports_match__1___rarg(lean_object*, lean_object*);
+lean_object* l_IO_getStdout___at_Lean_Elab_printDeps___spec__3(lean_object*);
 lean_object* l_Lean_Elab_headerToImports___closed__3;
-lean_object* l_IO_println___at_Lean_HasRepr_hasEval___spec__1(lean_object*, lean_object*);
-lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Syntax_getId(lean_object*);
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_processHeader___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_print_deps(lean_object*, lean_object*);
 lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
 lean_object* l_Lean_FileMap_ofString(lean_object*);
-lean_object* l_List_forM___main___at_Lean_Elab_printDeps___spec__1___boxed(lean_object*, lean_object*);
 lean_object* lean_mk_empty_environment(uint32_t, lean_object*);
 lean_object* lean_import_modules(lean_object*, uint32_t, lean_object*);
-extern lean_object* l_Lean_Syntax_inhabited;
 lean_object* l_Std_PersistentArray_push___rarg(lean_object*, lean_object*);
+lean_object* l_List_forInAux___main___at_Lean_Elab_printDeps___spec__4(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getArgs(lean_object*);
+lean_object* lean_get_stdout(lean_object*);
+lean_object* l_IO_print___at_Lean_Elab_printDeps___spec__2(lean_object*, lean_object*);
 lean_object* lean_parse_imports(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getPos(lean_object*);
 uint8_t l_Lean_Syntax_isNone(lean_object*);
 lean_object* l_Array_toList___rarg(lean_object*);
 lean_object* l_Lean_Elab_parseImports(lean_object*, lean_object*, lean_object*);
-lean_object* l_List_forM___main___at_Lean_Elab_printDeps___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
-lean_object* l_Lean_Syntax_asNode(lean_object*);
+lean_object* l_Lean_Elab_parseImportsExport_match__1___rarg(lean_object*, lean_object*);
+lean_object* l_Lean_Elab_parseImportsExport_match__1(lean_object*);
 extern lean_object* l_Std_Range___kind_term____x40_Init_Data_Range___hyg_111____closed__6;
 lean_object* l_List_map___main___at_Lean_Elab_headerToImports___spec__1(lean_object* x_1) {
 _start:
@ -66,7 +71,7 @@ uint8_t x_3;
 x_3 = !lean_is_exclusive(x_1);
 if (x_3 == 0)
 {
-lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 
 x_4 = lean_ctor_get(x_1, 0);
 x_5 = lean_ctor_get(x_1, 1);
 x_6 = lean_unsigned_to_nat(1u);
@ -74,71 +79,75 @@ x_7 = l_Lean_Syntax_getArg(x_4, x_6);
 x_8 = l_Lean_Syntax_isNone(x_7);
 lean_dec(x_7);
 x_9 = lean_unsigned_to_nat(2u);
-x_10 = l_Lean_Syntax_getIdAt(x_4, x_9);
+x_10 = l_Lean_Syntax_getArg(x_4, x_9);
 lean_dec(x_4);
-x_11 = l_List_map___main___at_Lean_Elab_headerToImports___spec__1(x_5);
+x_11 = l_Lean_Syntax_getId(x_10);
+lean_dec(x_10);
+x_12 = l_List_map___main___at_Lean_Elab_headerToImports___spec__1(x_5);
 if (x_8 == 0)
 {
-uint8_t x_12; lean_object* x_13; 
-x_12 = 1;
-x_13 = lean_alloc_ctor(0, 1, 1);
-lean_ctor_set(x_13, 0, x_10);
-lean_ctor_set_uint8(x_13, sizeof(void*)*1, x_12);
-lean_ctor_set(x_1, 1, x_11);
-lean_ctor_set(x_1, 0, x_13);
+uint8_t x_13; lean_object* x_14; 
+x_13 = 1;
+x_14 = lean_alloc_ctor(0, 1, 1);
+lean_ctor_set(x_14, 0, x_11);
+lean_ctor_set_uint8(x_14, sizeof(void*)*1, x_13);
+lean_ctor_set(x_1, 1, x_12);
+lean_ctor_set(x_1, 0, x_14);
 return x_1;
 }
 else
 {
-uint8_t x_14; lean_object* x_15; 
-x_14 = 0;
-x_15 = lean_alloc_ctor(0, 1, 1);
-lean_ctor_set(x_15, 0, x_10);
-lean_ctor_set_uint8(x_15, sizeof(void*)*1, x_14);
-lean_ctor_set(x_1, 1, x_11);
-lean_ctor_set(x_1, 0, x_15);
+uint8_t x_15; lean_object* x_16; 
+x_15 = 0;
+x_16 = lean_alloc_ctor(0, 1, 1);
+lean_ctor_set(x_16, 0, x_11);
+lean_ctor_set_uint8(x_16, sizeof(void*)*1, x_15);
+lean_ctor_set(x_1, 1, x_12);
+lean_ctor_set(x_1, 0, x_16);
 return x_1;
 }
 }
 else
 {
-lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; uint8_t x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; 
-x_16 = lean_ctor_get(x_1, 0);
-x_17 = lean_ctor_get(x_1, 1);
+lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; uint8_t x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; 
+x_17 = lean_ctor_get(x_1, 0);
+x_18 = lean_ctor_get(x_1, 1);
+lean_inc(x_18);
 lean_inc(x_17);
-lean_inc(x_16);
 lean_dec(x_1);
-x_18 = lean_unsigned_to_nat(1u);
-x_19 = l_Lean_Syntax_getArg(x_16, x_18);
-x_20 = l_Lean_Syntax_isNone(x_19);
-lean_dec(x_19);
-x_21 = lean_unsigned_to_nat(2u);
-x_22 = l_Lean_Syntax_getIdAt(x_16, x_21);
-lean_dec(x_16);
-x_23 = l_List_map___main___at_Lean_Elab_headerToImports___spec__1(x_17);
-if (x_20 == 0)
+x_19 = lean_unsigned_to_nat(1u);
+x_20 = l_Lean_Syntax_getArg(x_17, x_19);
+x_21 = l_Lean_Syntax_isNone(x_20);
+lean_dec(x_20);
+x_22 = lean_unsigned_to_nat(2u);
+x_23 = l_Lean_Syntax_getArg(x_17, x_22);
+lean_dec(x_17);
+x_24 = l_Lean_Syntax_getId(x_23);
+lean_dec(x_23);
+x_25 = l_List_map___main___at_Lean_Elab_headerToImports___spec__1(x_18);
+if (x_21 == 0)
 {
-uint8_t x_24; lean_object* x_25; lean_object* x_26; 
-x_24 = 1;
-x_25 = lean_alloc_ctor(0, 1, 1);
-lean_ctor_set(x_25, 0, x_22);
-lean_ctor_set_uint8(x_25, sizeof(void*)*1, x_24);
-x_26 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_26, 0, x_25);
-lean_ctor_set(x_26, 1, x_23);
-return x_26;
+uint8_t x_26; lean_object* x_27; lean_object* x_28; 
+x_26 = 1;
+x_27 = lean_alloc_ctor(0, 1, 1);
+lean_ctor_set(x_27, 0, x_24);
+lean_ctor_set_uint8(x_27, sizeof(void*)*1, x_26);
+x_28 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_28, 0, x_27);
+lean_ctor_set(x_28, 1, x_25);
+return x_28;
 }
 else
 {
-uint8_t x_27; lean_object* x_28; lean_object* x_29; 
-x_27 = 0;
-x_28 = lean_alloc_ctor(0, 1, 1);
-lean_ctor_set(x_28, 0, x_22);
-lean_ctor_set_uint8(x_28, sizeof(void*)*1, x_27);
-x_29 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_29, 0, x_28);
-lean_ctor_set(x_29, 1, x_23);
-return x_29;
+uint8_t x_29; lean_object* x_30; lean_object* x_31; 
+x_29 = 0;
+x_30 = lean_alloc_ctor(0, 1, 1);
+lean_ctor_set(x_30, 0, x_24);
+lean_ctor_set_uint8(x_30, sizeof(void*)*1, x_29);
+x_31 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_31, 0, x_30);
+lean_ctor_set(x_31, 1, x_25);
+return x_31;
 }
 }
 }
@ -181,45 +190,31 @@ return x_3;
 lean_object* l_Lean_Elab_headerToImports(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7; 
-x_2 = l_Lean_Syntax_asNode(x_1);
-x_3 = lean_ctor_get(x_2, 1);
-lean_inc(x_3);
-lean_dec(x_2);
-x_4 = l_Lean_Syntax_inhabited;
-x_5 = lean_unsigned_to_nat(0u);
-x_6 = lean_array_get(x_4, x_3, x_5);
-x_7 = l_Lean_Syntax_isNone(x_6);
-lean_dec(x_6);
-if (x_7 == 0)
-{
-lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; 
-x_8 = lean_box(0);
-x_9 = lean_unsigned_to_nat(1u);
-x_10 = lean_array_get(x_4, x_3, x_9);
+lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; 
+x_2 = lean_unsigned_to_nat(0u);
+x_3 = l_Lean_Syntax_getArg(x_1, x_2);
+x_4 = l_Lean_Syntax_isNone(x_3);
 lean_dec(x_3);
-x_11 = l_Lean_Syntax_getArgs(x_10);
-lean_dec(x_10);
-x_12 = l_Array_toList___rarg(x_11);
-lean_dec(x_11);
-x_13 = l_List_map___main___at_Lean_Elab_headerToImports___spec__1(x_12);
-x_14 = l_List_append___rarg(x_8, x_13);
-return x_14;
+x_5 = lean_unsigned_to_nat(1u);
+x_6 = l_Lean_Syntax_getArg(x_1, x_5);
+x_7 = l_Lean_Syntax_getArgs(x_6);
+lean_dec(x_6);
+x_8 = l_Array_toList___rarg(x_7);
+lean_dec(x_7);
+x_9 = l_List_map___main___at_Lean_Elab_headerToImports___spec__1(x_8);
+if (x_4 == 0)
+{
+lean_object* x_10; lean_object* x_11; 
+x_10 = lean_box(0);
+x_11 = l_List_append___rarg(x_10, x_9);
+return x_11;
 }
 else
 {
-lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; 
-x_15 = lean_unsigned_to_nat(1u);
-x_16 = lean_array_get(x_4, x_3, x_15);
-lean_dec(x_3);
-x_17 = l_Lean_Syntax_getArgs(x_16);
-lean_dec(x_16);
-x_18 = l_Array_toList___rarg(x_17);
-lean_dec(x_17);
-x_19 = l_List_map___main___at_Lean_Elab_headerToImports___spec__1(x_18);
-x_20 = l_Lean_Elab_headerToImports___closed__3;
-x_21 = l_List_append___rarg(x_20, x_19);
-return x_21;
+lean_object* x_12; lean_object* x_13; 
+x_12 = l_Lean_Elab_headerToImports___closed__3;
+x_13 = l_List_append___rarg(x_12, x_9);
+return x_13;
 }
 }
 }
@ -451,6 +446,32 @@ lean_dec(x_1);
 return x_7;
 }
 }
+lean_object* l_Lean_Elab_parseImports_match__1___rarg(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
+x_3 = lean_ctor_get(x_1, 1);
+lean_inc(x_3);
+x_4 = lean_ctor_get(x_1, 0);
+lean_inc(x_4);
+lean_dec(x_1);
+x_5 = lean_ctor_get(x_3, 0);
+lean_inc(x_5);
+x_6 = lean_ctor_get(x_3, 1);
+lean_inc(x_6);
+lean_dec(x_3);
+x_7 = lean_apply_3(x_2, x_4, x_5, x_6);
+return x_7;
+}
+}
+lean_object* l_Lean_Elab_parseImports_match__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_Elab_parseImports_match__1___rarg), 2, 0);
+return x_2;
+}
+}
 static lean_object* _init_l_Lean_Elab_parseImports___closed__1() {
 _start:
 {
@ -834,6 +855,32 @@ return x_111;
 }
 }
 }
+lean_object* l_Lean_Elab_parseImportsExport_match__1___rarg(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
+x_3 = lean_ctor_get(x_1, 1);
+lean_inc(x_3);
+x_4 = lean_ctor_get(x_1, 0);
+lean_inc(x_4);
+lean_dec(x_1);
+x_5 = lean_ctor_get(x_3, 0);
+lean_inc(x_5);
+x_6 = lean_ctor_get(x_3, 1);
+lean_inc(x_6);
+lean_dec(x_3);
+x_7 = lean_apply_3(x_2, x_4, x_5, x_6);
+return x_7;
+}
+}
+lean_object* l_Lean_Elab_parseImportsExport_match__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_Elab_parseImportsExport_match__1___rarg), 2, 0);
+return x_2;
+}
+}
 lean_object* lean_parse_imports(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
@ -993,25 +1040,87 @@ return x_38;
 }
 }
 }
-lean_object* l_List_forM___main___at_Lean_Elab_printDeps___spec__1(lean_object* x_1, lean_object* x_2) {
+lean_object* l_IO_getStdout___at_Lean_Elab_printDeps___spec__3(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_get_stdout(x_1);
+return x_2;
+}
+}
+lean_object* l_IO_print___at_Lean_Elab_printDeps___spec__2(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = lean_get_stdout(x_2);
+if (lean_obj_tag(x_3) == 0)
+{
+lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
+x_4 = lean_ctor_get(x_3, 0);
+lean_inc(x_4);
+x_5 = lean_ctor_get(x_3, 1);
+lean_inc(x_5);
+lean_dec(x_3);
+x_6 = lean_ctor_get(x_4, 5);
+lean_inc(x_6);
+lean_dec(x_4);
+x_7 = lean_apply_2(x_6, x_1, x_5);
+return x_7;
+}
+else
+{
+uint8_t x_8; 
+lean_dec(x_1);
+x_8 = !lean_is_exclusive(x_3);
+if (x_8 == 0)
+{
+return x_3;
+}
+else
+{
+lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+x_9 = lean_ctor_get(x_3, 0);
+x_10 = lean_ctor_get(x_3, 1);
+lean_inc(x_10);
+lean_inc(x_9);
+lean_dec(x_3);
+x_11 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_11, 0, x_9);
+lean_ctor_set(x_11, 1, x_10);
+return x_11;
+}
+}
+}
+}
+lean_object* l_IO_println___at_Lean_Elab_printDeps___spec__1(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+uint32_t x_3; lean_object* x_4; lean_object* x_5; 
+x_3 = 10;
+x_4 = lean_string_push(x_1, x_3);
+x_5 = l_IO_print___at_Lean_Elab_printDeps___spec__2(x_4, x_2);
+return x_5;
+}
+}
+lean_object* l_List_forInAux___main___at_Lean_Elab_printDeps___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
 if (lean_obj_tag(x_1) == 0)
 {
-lean_object* x_3; lean_object* x_4; 
-x_3 = lean_box(0);
+lean_object* x_4; 
 x_4 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_4, 0, x_3);
-lean_ctor_set(x_4, 1, x_2);
+lean_ctor_set(x_4, 0, x_2);
+lean_ctor_set(x_4, 1, x_3);
 return x_4;
 }
 else
 {
 lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; 
+lean_dec(x_2);
 x_5 = lean_ctor_get(x_1, 0);
 x_6 = lean_ctor_get(x_1, 1);
 x_7 = lean_ctor_get(x_5, 0);
-x_8 = l_Lean_findOLean(x_7, x_2);
+x_8 = l_Lean_findOLean(x_7, x_3);
 if (lean_obj_tag(x_8) == 0)
 {
 lean_object* x_9; lean_object* x_10; lean_object* x_11; 
@ -1020,60 +1129,62 @@ lean_inc(x_9);
 x_10 = lean_ctor_get(x_8, 1);
 lean_inc(x_10);
 lean_dec(x_8);
-x_11 = l_IO_println___at_Lean_HasRepr_hasEval___spec__1(x_9, x_10);
+x_11 = l_IO_println___at_Lean_Elab_printDeps___spec__1(x_9, x_10);
 if (lean_obj_tag(x_11) == 0)
 {
-lean_object* x_12; 
+lean_object* x_12; lean_object* x_13; 
 x_12 = lean_ctor_get(x_11, 1);
 lean_inc(x_12);
 lean_dec(x_11);
+x_13 = lean_box(0);
 x_1 = x_6;
-x_2 = x_12;
+x_2 = x_13;
+x_3 = x_12;
 goto _start;
 }
 else
 {
-uint8_t x_14; 
-x_14 = !lean_is_exclusive(x_11);
-if (x_14 == 0)
+uint8_t x_15; 
+x_15 = !lean_is_exclusive(x_11);
+if (x_15 == 0)
 {
 return x_11;
 }
 else
 {
-lean_object* x_15; lean_object* x_16; lean_object* x_17; 
-x_15 = lean_ctor_get(x_11, 0);
-x_16 = lean_ctor_get(x_11, 1);
+lean_object* x_16; lean_object* x_17; lean_object* x_18; 
+x_16 = lean_ctor_get(x_11, 0);
+x_17 = lean_ctor_get(x_11, 1);
+lean_inc(x_17);
 lean_inc(x_16);
-lean_inc(x_15);
 lean_dec(x_11);
-x_17 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_17, 0, x_15);
-lean_ctor_set(x_17, 1, x_16);
-return x_17;
+x_18 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_18, 0, x_16);
+lean_ctor_set(x_18, 1, x_17);
+return x_18;
 }
 }
 }
 else
 {
-uint8_t x_18; 
-x_18 = !lean_is_exclusive(x_8);
-if (x_18 == 0)
+uint8_t x_19; 
+x_19 = !lean_is_exclusive(x_8);
+if (x_19 == 0)
 {
 return x_8;
 }
 else
 {
-lean_object* x_19; lean_object* x_20; lean_object* x_21; 
-x_19 = lean_ctor_get(x_8, 0);
-x_20 = lean_ctor_get(x_8, 1);
+lean_object* x_20; lean_object* x_21; lean_object* x_22; 
+x_20 = lean_ctor_get(x_8, 0);
+x_21 = lean_ctor_get(x_8, 1);
+lean_inc(x_21);
 lean_inc(x_20);
-lean_inc(x_19);
 lean_dec(x_8);
-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;
+x_22 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_22, 0, x_20);
+lean_ctor_set(x_22, 1, x_21);
+return x_22;
 }
 }
 }
@ -1082,19 +1193,63 @@ return x_21;
 lean_object* lean_print_deps(lean_object* x_1, lean_object* x_2) {
 _start:
 {
-lean_object* x_3; 
-x_3 = l_List_forM___main___at_Lean_Elab_printDeps___spec__1(x_1, x_2);
+lean_object* x_3; lean_object* x_4; 
+x_3 = lean_box(0);
+x_4 = l_List_forInAux___main___at_Lean_Elab_printDeps___spec__4(x_1, x_3, x_2);
 lean_dec(x_1);
-return x_3;
+if (lean_obj_tag(x_4) == 0)
+{
+uint8_t x_5; 
+x_5 = !lean_is_exclusive(x_4);
+if (x_5 == 0)
+{
+return x_4;
+}
+else
+{
+lean_object* x_6; lean_object* x_7; lean_object* x_8; 
+x_6 = lean_ctor_get(x_4, 0);
+x_7 = lean_ctor_get(x_4, 1);
+lean_inc(x_7);
+lean_inc(x_6);
+lean_dec(x_4);
+x_8 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_8, 0, x_6);
+lean_ctor_set(x_8, 1, x_7);
+return x_8;
 }
 }
-lean_object* l_List_forM___main___at_Lean_Elab_printDeps___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
+else
+{
+uint8_t x_9; 
+x_9 = !lean_is_exclusive(x_4);
+if (x_9 == 0)
+{
+return x_4;
+}
+else
+{
+lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+x_10 = lean_ctor_get(x_4, 0);
+x_11 = lean_ctor_get(x_4, 1);
+lean_inc(x_11);
+lean_inc(x_10);
+lean_dec(x_4);
+x_12 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_12, 0, x_10);
+lean_ctor_set(x_12, 1, x_11);
+return x_12;
+}
+}
+}
+}
+lean_object* l_List_forInAux___main___at_Lean_Elab_printDeps___spec__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
-lean_object* x_3; 
-x_3 = l_List_forM___main___at_Lean_Elab_printDeps___spec__1(x_1, x_2);
+lean_object* x_4; 
+x_4 = l_List_forInAux___main___at_Lean_Elab_printDeps___spec__4(x_1, x_2, x_3);
 lean_dec(x_1);
-return x_3;
+return x_4;
 }
 }
 lean_object* initialize_Init(lean_object*);
--- a/stage0/stdlib/Lean/Elab/Inductive.c
+++ b/stage0/stdlib/Lean/Elab/Inductive.c
@ -33,6 +33,7 @@ lean_object* l_Array_forMAux___main___at___private_Lean_Elab_Inductive_4__checkL
 lean_object* l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___closed__1;
 lean_object* l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_checkValidInductiveModifier___closed__6;
+lean_object* l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__4;
 lean_object* l_List_mapM___main___at___private_Lean_Elab_Inductive_16__elabCtors___spec__2___lambda__1___closed__4;
 lean_object* l_Lean_mkSort(lean_object*);
 lean_object* l_List_mapM___main___at___private_Lean_Elab_Inductive_31__replaceIndFVarsWithConsts___spec__2___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*);
@ -65,6 +66,7 @@ extern lean_object* l_Lean_Elab_Attribute_inhabited;
 lean_object* l___private_Lean_Elab_Inductive_35__mkInductiveDecl___lambda__3(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_Inductive_14__withInductiveLocalDecls___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*);
 extern lean_object* l_Std_HashMap_inhabited___closed__1;
+lean_object* l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__6;
 lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
 lean_object* l___private_Lean_Elab_Inductive_28__updateParams___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Meta_InferType_22__isTypeFormerTypeImp___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -104,6 +106,7 @@ lean_object* l_List_mapM___main___at___private_Lean_Elab_Inductive_31__replaceIn
 lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
 extern lean_object* l_Lean_Prod_hasQuote___rarg___closed__2;
+lean_object* l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__5;
 lean_object* l_Array_forMAux___main___at___private_Lean_Elab_Inductive_4__checkLevelNames___spec__1___closed__2;
 lean_object* lean_string_append(lean_object*, lean_object*);
 lean_object* l_List_forM___main___at___private_Lean_Elab_Inductive_24__traceIndTypes___spec__4___closed__1;
@ -167,7 +170,6 @@ lean_object* l___private_Lean_Elab_Inductive_13__withInductiveLocalDeclsAux___ma
 lean_object* lean_array_fget(lean_object*, lean_object*);
 lean_object* l_Nat_forMAux___main___at___private_Lean_Elab_Inductive_16__elabCtors___spec__1___closed__5;
 lean_object* l___private_Lean_Elab_Inductive_20__collectUniversesFromCtorTypeAux___main___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* l_Lean_Meta_forallTelescopeCompatibleAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Expr_Inhabited___closed__1;
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Inductive_23__updateResultingUniverse(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -257,7 +259,6 @@ lean_object* l_Lean_Elab_Command_checkValidCtorModifier___closed__6;
 lean_object* l___private_Lean_Elab_Inductive_17__levelMVarToParamAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Nat_forMAux___main___at___private_Lean_Elab_Inductive_16__elabCtors___spec__1___closed__4;
 lean_object* lean_mk_no_confusion(lean_object*, lean_object*);
-extern lean_object* l_Lean_Meta_forallTelescopeCompatibleAux___main___rarg___closed__18;
 lean_object* l_Lean_Elab_Command_shouldInferResultUniverse___closed__5;
 lean_object* l___private_Lean_Meta_Basic_20__forallTelescopeReducingImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_Term_Lean_Ref___closed__2;
@ -367,6 +368,7 @@ lean_object* lean_mk_rec_on(lean_object*, lean_object*);
 lean_object* l_Array_forMAux___main___at___private_Lean_Elab_Inductive_3__checkUnsafe___spec__1___closed__2;
 lean_object* l_Lean_Expr_ReplaceLevelImpl_replaceUnsafeM___main___at___private_Lean_Elab_Inductive_23__updateResultingUniverse___spec__1(lean_object*, size_t, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Inductive_31__replaceIndFVarsWithConsts___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_Meta_forallTelescopeCompatibleAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_toList___rarg(lean_object*);
 lean_object* l_Lean_Elab_Command_checkValidInductiveModifier___closed__1;
 lean_object* l___private_Lean_Elab_Inductive_33__applyInferMod___boxed(lean_object*, lean_object*, lean_object*);
@ -2152,6 +2154,34 @@ lean_ctor_set(x_2, 0, x_1);
 return x_2;
 }
 }
+static lean_object* _init_l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__4() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("expected type");
+return x_1;
+}
+}
+static lean_object* _init_l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__5() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__4;
+x_2 = lean_alloc_ctor(2, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
+static lean_object* _init_l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__6() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; 
+x_1 = l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__5;
+x_2 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_2, 0, x_1);
+return x_2;
+}
+}
 lean_object* l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
 _start:
 {
@ -2187,7 +2217,7 @@ x_18 = l_Lean_MessageData_ofList___closed__3;
 x_19 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_19, 0, x_17);
 lean_ctor_set(x_19, 1, x_18);
-x_20 = l_Lean_Meta_forallTelescopeCompatibleAux___main___rarg___closed__18;
+x_20 = l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__6;
 x_21 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_21, 0, x_19);
 lean_ctor_set(x_21, 1, x_20);
@ -2337,7 +2367,7 @@ x_11 = lean_alloc_closure((void*)(l___private_Lean_Elab_Inductive_9__checkParams
 lean_closure_set(x_11, 0, x_4);
 lean_closure_set(x_11, 1, x_5);
 x_12 = l_Array_empty___closed__1;
-x_13 = l_Lean_Meta_forallTelescopeCompatibleAux___main___rarg(x_11, x_3, x_1, x_2, x_12, x_6, x_7, x_8, x_9, x_10);
+x_13 = l_Lean_Meta_forallTelescopeCompatibleAux___rarg(x_11, x_3, x_1, x_2, x_12, x_6, x_7, x_8, x_9, x_10);
 if (lean_obj_tag(x_13) == 0)
 {
 uint8_t x_14; 
@ -14341,6 +14371,12 @@ l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed
 lean_mark_persistent(l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__2);
 l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__3 = _init_l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__3();
 lean_mark_persistent(l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__3);
+l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__4 = _init_l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__4();
+lean_mark_persistent(l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__4);
+l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__5 = _init_l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__5();
+lean_mark_persistent(l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__5);
+l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__6 = _init_l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__6();
+lean_mark_persistent(l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___lambda__1___closed__6);
 l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___closed__1 = _init_l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___closed__1();
 lean_mark_persistent(l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___closed__1);
 l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___closed__2 = _init_l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___closed__2();
--- a/stage0/stdlib/Lean/Elab/LetRec.c
+++ b/stage0/stdlib/Lean/Elab/LetRec.c
--- a/stage0/stdlib/Lean/Elab/MutualDef.c
+++ b/stage0/stdlib/Lean/Elab/MutualDef.c
@ -22,6 +22,7 @@ lean_object* l_List_forM___main___at___private_Lean_Elab_MutualDef_20__checkLetR
 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_Lean_extractMacroScopes(lean_object*);
 lean_object* l_Lean_Elab_logTrace___at___private_Lean_Elab_MutualDef_35__mkClosureForAux___main___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+size_t l_USize_add(size_t, size_t);
 lean_object* l_Lean_Meta_forallBoundedTelescope___at_Lean_Elab_Term_elabLetDeclAux___spec__1___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* l___private_Lean_Elab_MutualDef_35__mkClosureForAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_getLocalDecl___at___private_Lean_Elab_MutualDef_35__mkClosureForAux___main___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -74,6 +75,7 @@ lean_object* l_Lean_Elab_elabModifiers___at_Lean_Elab_Command_elabMutualDef___sp
 lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_MutualClosure_main___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_MutualDef_3__check___closed__22;
 lean_object* l_Lean_Meta_findLocalDecl_x3f___at___private_Lean_Elab_MutualDef_19__getFunName___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabMutualDef___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_checkNotAlreadyDeclared___rarg___lambda__2___closed__3;
 extern lean_object* l_Array_empty___closed__1;
 lean_object* l_Lean_Meta_resetZetaFVarIds___at_Lean_Elab_Term_MutualClosure_main___spec__2___boxed(lean_object*, lean_object*, lean_object*);
@ -90,7 +92,6 @@ lean_object* l___private_Lean_Elab_MutualDef_27__merge(lean_object*, lean_object
 lean_object* l_Lean_MessageData_arrayExpr_toMessageData___main(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_LocalContext_get_x21(lean_object*, lean_object*);
 lean_object* lean_private_to_user_name(lean_object*);
-extern lean_object* l_Lean_MessageData_arrayExpr_toMessageData___main___closed__1;
 lean_object* l_Lean_Elab_elabAttrs___at_Lean_Elab_Command_elabMutualDef___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_reverseAux___main___rarg(lean_object*, lean_object*);
 uint8_t l_Array_anyRangeMAux___main___at_Lean_Elab_Term_MutualClosure_getModifiersForLetRecs___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
@ -125,7 +126,6 @@ lean_object* l_Lean_Elab_mkDeclName___at___private_Lean_Elab_MutualDef_6__elabHe
 extern lean_object* l_String_splitAux___main___closed__1;
 lean_object* l_Lean_Elab_Term_MutualClosure_main(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_Nat_foldAux___main___at_Lean_Elab_Term_MutualClosure_insertReplacementForMainFns___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_Command_elabMutualDef___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_indexOfAux___main___at_Lean_LocalContext_erase___spec__3(lean_object*, lean_object*, lean_object*);
 lean_object* lean_string_utf8_byte_size(lean_object*);
 lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_MutualDef_10__elabFunValues___spec__1___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -138,6 +138,7 @@ lean_object* l_Lean_Elab_elabModifiers___at_Lean_Elab_Command_elabMutualDef___sp
 uint8_t l_Lean_LocalContext_contains(lean_object*, lean_object*);
 uint8_t l_Lean_Elab_DefKind_isExample(uint8_t);
 lean_object* l_Lean_Elab_Term_MutualClosure_insertReplacementForMainFns___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+uint8_t l_USize_decLt(size_t, size_t);
 lean_object* l_Lean_Meta_getZetaFVarIds___at___private_Lean_Elab_MutualDef_35__mkClosureForAux___main___spec__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_forM___main___at___private_Lean_Elab_MutualDef_11__collectUsed___spec__3___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_MutualDef_35__mkClosureForAux___main___closed__2;
@ -236,6 +237,7 @@ uint8_t l_Array_anyRangeMAux___main___at_Lean_Elab_Term_MutualClosure_getModifie
 lean_object* l_Lean_Meta_forallBoundedTelescope___at_Lean_Elab_Term_elabLetDeclAux___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_Command_mkDefViewOfConstant___closed__8;
 lean_object* l_Lean_Elab_elabModifiers___at_Lean_Elab_Command_elabMutualDef___spec__1___closed__5;
+lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabMutualDef___spec__5(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_MutualDef_29__fixpoint(lean_object*);
 lean_object* l_Lean_Meta_instantiateForall___at___private_Lean_Elab_MutualDef_37__mkLetRecClosureFor___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_umapMAux___main___at___private_Lean_Elab_MutualDef_35__mkClosureForAux___main___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -319,6 +321,7 @@ uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
 lean_object* l___private_Lean_Elab_MutualDef_28__updateUsedVarsOf(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_MutualDef_2__checkKinds___closed__5;
 lean_object* l_Lean_Elab_log___at___private_Lean_Elab_MutualDef_35__mkClosureForAux___main___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+size_t lean_usize_of_nat(lean_object*);
 lean_object* l_Nat_foldMAux___main___at_Lean_Elab_Term_MutualClosure_pushMain___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_replaceFVarIdAtLocalDecl(lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Elab_DefKind_isTheorem(uint8_t);
@ -377,6 +380,7 @@ lean_object* l_Lean_Macro_throwError___rarg(lean_object*, lean_object*, lean_obj
 lean_object* l___private_Lean_Elab_MutualDef_1__checkModifiers(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_MutualDef_21__mkInitialUsedFVarsMap___spec__3___lambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_LocalDecl_index(lean_object*);
+lean_object* l_Lean_Syntax_getSepArgs(lean_object*);
 uint8_t l_Lean_isAttribute(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_MutualDef_5__elabFunType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_erase___at___private_Lean_Elab_MutualDef_35__mkClosureForAux___main___spec__1___boxed(lean_object*, lean_object*);
@ -487,7 +491,6 @@ lean_object* l___private_Lean_Elab_MutualDef_3__check___closed__10;
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_MutualClosure_main___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_mkDefView(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l_Lean_Elab_elabAttr___rarg___lambda__2___closed__3;
 extern lean_object* l_Lean_Elab_mkDeclName___rarg___closed__3;
 extern lean_object* l_Lean_Elab_PreDefinition_inhabited___closed__1;
 lean_object* l___private_Lean_Elab_MutualDef_2__checkKinds___closed__1;
@ -515,6 +518,7 @@ lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_MutualDef_6__el
 lean_object* l_Lean_Elab_elabModifiers___at_Lean_Elab_Command_elabMutualDef___spec__1___closed__11;
 uint8_t l___private_Lean_Elab_MutualDef_14__isExample(lean_object*);
 lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Elab_Term_20__elabImplicitLambda___main___spec__1___rarg(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_Lean_Elab_elabAttr___rarg___lambda__5___closed__2;
 lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_MutualDef_3__check___closed__23;
 lean_object* l_Lean_mkConst(lean_object*, lean_object*);
@ -523,9 +527,9 @@ lean_object* l_Nat_foldMAux___main___at_Lean_Elab_Term_MutualClosure_pushMain___
 lean_object* l_Lean_Elab_elabModifiers___at_Lean_Elab_Command_elabMutualDef___spec__1___closed__12;
 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_Elab_Term_MutualClosure_getKindForLetRecs___boxed(lean_object*);
+extern lean_object* l_Lean_Elab_elabAttr___rarg___lambda__5___closed__3;
 lean_object* l_Array_anyRangeMAux___main___at_Lean_Elab_Term_MutualClosure_getKindForLetRecs___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_MutualDef_8__withFunLocalDecls___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_Command_elabMutualDef___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_MutualDef_35__mkClosureForAux___main___closed__5;
 lean_object* l_Lean_Elab_DefViewElabHeader_inhabited;
 lean_object* l___private_Lean_Elab_MutualDef_13__withUsedWhen___rarg(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*);
@ -14603,11 +14607,11 @@ lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean
 lean_free_object(x_36);
 x_42 = lean_alloc_ctor(4, 1, 0);
 lean_ctor_set(x_42, 0, x_35);
-x_43 = l_Lean_Elab_elabAttr___rarg___lambda__2___closed__3;
+x_43 = l_Lean_Elab_elabAttr___rarg___lambda__5___closed__2;
 x_44 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_44, 0, x_43);
 lean_ctor_set(x_44, 1, x_42);
-x_45 = l_Lean_MessageData_arrayExpr_toMessageData___main___closed__1;
+x_45 = l_Lean_Elab_elabAttr___rarg___lambda__5___closed__3;
 x_46 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_46, 0, x_44);
 lean_ctor_set(x_46, 1, x_45);
@ -14680,11 +14684,11 @@ if (x_62 == 0)
 lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; 
 x_63 = lean_alloc_ctor(4, 1, 0);
 lean_ctor_set(x_63, 0, x_35);
-x_64 = l_Lean_Elab_elabAttr___rarg___lambda__2___closed__3;
+x_64 = l_Lean_Elab_elabAttr___rarg___lambda__5___closed__2;
 x_65 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_65, 0, x_64);
 lean_ctor_set(x_65, 1, x_63);
-x_66 = l_Lean_MessageData_arrayExpr_toMessageData___main___closed__1;
+x_66 = l_Lean_Elab_elabAttr___rarg___lambda__5___closed__3;
 x_67 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_67, 0, x_65);
 lean_ctor_set(x_67, 1, x_66);
@ -14748,44 +14752,41 @@ return x_81;
 }
 }
 }
-lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_Command_elabMutualDef___spec__5(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_Lean_Elab_Command_elabMutualDef___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:
 {
-lean_object* x_8; uint8_t x_9; 
-x_8 = lean_array_get_size(x_2);
-x_9 = lean_nat_dec_lt(x_3, x_8);
-lean_dec(x_8);
-if (x_9 == 0)
+uint8_t x_8; 
+x_8 = x_3 < x_2;
+if (x_8 == 0)
 {
-lean_object* x_10; 
+lean_object* x_9; 
 lean_dec(x_5);
-lean_dec(x_3);
-x_10 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_10, 0, x_4);
-lean_ctor_set(x_10, 1, x_7);
-return x_10;
+x_9 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_9, 0, x_4);
+lean_ctor_set(x_9, 1, x_7);
+return x_9;
 }
 else
 {
-lean_object* x_11; lean_object* x_12; 
-x_11 = lean_array_fget(x_2, x_3);
+lean_object* x_10; lean_object* x_11; 
+x_10 = lean_array_uget(x_1, x_3);
 lean_inc(x_5);
-x_12 = l_Lean_Elab_elabAttr___at_Lean_Elab_Command_elabMutualDef___spec__4(x_11, x_5, x_6, x_7);
-lean_dec(x_11);
-if (lean_obj_tag(x_12) == 0)
+x_11 = l_Lean_Elab_elabAttr___at_Lean_Elab_Command_elabMutualDef___spec__4(x_10, x_5, x_6, x_7);
+lean_dec(x_10);
+if (lean_obj_tag(x_11) == 0)
 {
-lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; 
-x_13 = lean_ctor_get(x_12, 0);
+lean_object* x_12; lean_object* x_13; lean_object* x_14; size_t x_15; size_t x_16; 
+x_12 = lean_ctor_get(x_11, 0);
+lean_inc(x_12);
+x_13 = lean_ctor_get(x_11, 1);
 lean_inc(x_13);
-x_14 = lean_ctor_get(x_12, 1);
-lean_inc(x_14);
-lean_dec(x_12);
-x_15 = lean_array_push(x_4, x_13);
-x_16 = lean_nat_add(x_3, x_1);
-lean_dec(x_3);
+lean_dec(x_11);
+x_14 = lean_array_push(x_4, x_12);
+x_15 = 1;
+x_16 = x_3 + x_15;
 x_3 = x_16;
-x_4 = x_15;
-x_7 = x_14;
+x_4 = x_14;
+x_7 = x_13;
 goto _start;
 }
 else
@ -14793,20 +14794,19 @@ else
 uint8_t x_18; 
 lean_dec(x_5);
 lean_dec(x_4);
-lean_dec(x_3);
-x_18 = !lean_is_exclusive(x_12);
+x_18 = !lean_is_exclusive(x_11);
 if (x_18 == 0)
 {
-return x_12;
+return x_11;
 }
 else
 {
 lean_object* x_19; lean_object* x_20; lean_object* x_21; 
-x_19 = lean_ctor_get(x_12, 0);
-x_20 = lean_ctor_get(x_12, 1);
+x_19 = lean_ctor_get(x_11, 0);
+x_20 = lean_ctor_get(x_11, 1);
 lean_inc(x_20);
 lean_inc(x_19);
-lean_dec(x_12);
+lean_dec(x_11);
 x_21 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_21, 0, x_19);
 lean_ctor_set(x_21, 1, x_20);
@ -14819,14 +14819,59 @@ return x_21;
 lean_object* l_Lean_Elab_elabAttrs___at_Lean_Elab_Command_elabMutualDef___spec__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
-lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; 
-x_5 = l_Lean_Syntax_getArgs(x_1);
-x_6 = lean_unsigned_to_nat(2u);
-x_7 = lean_unsigned_to_nat(0u);
-x_8 = l_Array_empty___closed__1;
-x_9 = l_Array_foldlStepMAux___main___at_Lean_Elab_Command_elabMutualDef___spec__5(x_6, x_5, x_7, x_8, x_2, x_3, x_4);
+lean_object* x_5; lean_object* x_6; size_t x_7; size_t x_8; lean_object* x_9; lean_object* x_10; 
+x_5 = l_Lean_Syntax_getSepArgs(x_1);
+x_6 = lean_array_get_size(x_5);
+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_Lean_Elab_Command_elabMutualDef___spec__5(x_5, x_7, x_8, x_9, x_2, x_3, x_4);
 lean_dec(x_5);
-return x_9;
+if (lean_obj_tag(x_10) == 0)
+{
+uint8_t x_11; 
+x_11 = !lean_is_exclusive(x_10);
+if (x_11 == 0)
+{
+return x_10;
+}
+else
+{
+lean_object* x_12; lean_object* x_13; lean_object* x_14; 
+x_12 = lean_ctor_get(x_10, 0);
+x_13 = lean_ctor_get(x_10, 1);
+lean_inc(x_13);
+lean_inc(x_12);
+lean_dec(x_10);
+x_14 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_14, 0, x_12);
+lean_ctor_set(x_14, 1, x_13);
+return x_14;
+}
+}
+else
+{
+uint8_t x_15; 
+x_15 = !lean_is_exclusive(x_10);
+if (x_15 == 0)
+{
+return x_10;
+}
+else
+{
+lean_object* x_16; lean_object* x_17; lean_object* x_18; 
+x_16 = lean_ctor_get(x_10, 0);
+x_17 = lean_ctor_get(x_10, 1);
+lean_inc(x_17);
+lean_inc(x_16);
+lean_dec(x_10);
+x_18 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_18, 0, x_16);
+lean_ctor_set(x_18, 1, x_17);
+return x_18;
+}
+}
 }
 }
 lean_object* l_Lean_Elab_elabDeclAttrs___at_Lean_Elab_Command_elabMutualDef___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
@ -20216,15 +20261,18 @@ lean_dec(x_1);
 return x_5;
 }
 }
-lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_Command_elabMutualDef___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) {
+lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabMutualDef___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:
 {
-lean_object* x_8; 
-x_8 = l_Array_foldlStepMAux___main___at_Lean_Elab_Command_elabMutualDef___spec__5(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
-lean_dec(x_6);
+size_t x_8; size_t x_9; lean_object* x_10; 
+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_Lean_Elab_Command_elabMutualDef___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_8;
+return x_10;
 }
 }
 lean_object* l_Lean_Elab_elabAttrs___at_Lean_Elab_Command_elabMutualDef___spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Main.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Main.c
@ -57,7 +57,6 @@ lean_object* l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_ensureNoUnass
 lean_object* l_Lean_Meta_collectMVarsAux___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__1;
 lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___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*);
-extern lean_object* l_Lean_Elab_Term_reportUnsolvedGoals___closed__3;
 lean_object* l___private_Lean_Util_SCC_1__getDataOf___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__7___boxed(lean_object*, lean_object*);
 lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_USize_decLt(size_t, size_t);
@ -72,6 +71,7 @@ lean_object* l_Lean_Expr_FoldConstsImpl_fold___main___at___private_Lean_Elab_Pre
 lean_object* l___private_Lean_Util_SCC_5__updateLowLinkOf___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__18(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__8___lambda__4___closed__2;
 lean_object* l_Lean_Elab_addAndCompileUnsafe(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l_Lean_Meta_forallTelescopeCompatibleAux___rarg___closed__13;
 lean_object* l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_isNonRecursive_match__1(lean_object*);
 lean_object* l_Std_AssocList_foldlM___main___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__16(lean_object*, lean_object*);
 lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___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*);
@ -369,7 +369,7 @@ x_26 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__L
 x_27 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_27, 0, x_26);
 lean_ctor_set(x_27, 1, x_25);
-x_28 = l_Lean_Elab_Term_reportUnsolvedGoals___closed__3;
+x_28 = l_Lean_Meta_forallTelescopeCompatibleAux___rarg___closed__13;
 x_29 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_29, 0, x_27);
 lean_ctor_set(x_29, 1, x_28);
@ -587,7 +587,7 @@ x_34 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__L
 x_35 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_35, 0, x_34);
 lean_ctor_set(x_35, 1, x_33);
-x_36 = l_Lean_Elab_Term_reportUnsolvedGoals___closed__3;
+x_36 = l_Lean_Meta_forallTelescopeCompatibleAux___rarg___closed__13;
 x_37 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_37, 0, x_35);
 lean_ctor_set(x_37, 1, x_36);
@ -4110,7 +4110,7 @@ x_21 = lean_ctor_get(x_14, 2);
 lean_inc(x_21);
 x_22 = lean_alloc_ctor(4, 1, 0);
 lean_ctor_set(x_22, 0, x_21);
-x_23 = l_Lean_Elab_Term_reportUnsolvedGoals___closed__3;
+x_23 = l_Lean_Meta_forallTelescopeCompatibleAux___rarg___closed__13;
 x_24 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_24, 0, x_23);
 lean_ctor_set(x_24, 1, x_22);
@ -4479,7 +4479,7 @@ lean_ctor_set(x_11, 1, x_10);
 x_12 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_12, 0, x_11);
 lean_ctor_set(x_12, 1, x_2);
-x_13 = l_Lean_Elab_Term_reportUnsolvedGoals___closed__3;
+x_13 = l_Lean_Meta_forallTelescopeCompatibleAux___rarg___closed__13;
 x_14 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_14, 0, x_12);
 lean_ctor_set(x_14, 1, x_13);
@ -5113,7 +5113,7 @@ lean_dec(x_96);
 x_98 = l_List_map___main___at_Lean_Elab_addPreDefinitions___spec__7(x_97);
 x_99 = l_Lean_MessageData_ofList(x_98);
 lean_dec(x_98);
-x_100 = l_Lean_Elab_Term_reportUnsolvedGoals___closed__3;
+x_100 = l_Lean_Meta_forallTelescopeCompatibleAux___rarg___closed__13;
 x_101 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_101, 0, x_100);
 lean_ctor_set(x_101, 1, x_99);
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Structural.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Structural.c
--- a/stage0/stdlib/Lean/Elab/Print.c
+++ b/stage0/stdlib/Lean/Elab/Print.c
@ -57,7 +57,6 @@ lean_object* l_Lean_MessageData_ofList(lean_object*);
 lean_object* l_Lean_Elab_Command_CollectAxioms_collect_match__2(lean_object*);
 lean_object* l_Lean_addMessageContextPartial___at_Lean_Elab_Command_Lean_AddMessageContext___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_String_splitAux___main___closed__1;
-extern lean_object* l_Lean_Elab_Term_reportUnsolvedGoals___closed__3;
 lean_object* l_Lean_Elab_Command_elabPrint___closed__4;
 lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkHeader_match__2___rarg(lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Command_elabPrint___closed__2;
@ -69,6 +68,7 @@ lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkHeader___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__2;
 lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkHeader___closed__1;
+extern lean_object* l_Lean_Meta_forallTelescopeCompatibleAux___rarg___closed__13;
 lean_object* l_Lean_getConstInfo___at___private_Lean_Elab_Print_0__Lean_Elab_Command_printInduct___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_printAxiomLike(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltin_Lean_Elab_Command_elabPrintAxioms(lean_object*);
@ -107,7 +107,6 @@ extern lean_object* l_Lean_throwUnknownConstant___rarg___closed__5;
 lean_object* l_Lean_Elab_Command_CollectAxioms_State_axioms___default;
 lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
 uint8_t l_Array_isEmpty___rarg(lean_object*);
-extern lean_object* l_Lean_Elab_syntaxNodeKindOfAttrParam___closed__6;
 lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkHeader(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_forM___main___at___private_Lean_Elab_Print_0__Lean_Elab_Command_printId___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_throwUnknownConstant___rarg___closed__3;
@ -186,6 +185,7 @@ extern lean_object* l_Lean_Elab_Term_resolveName___closed__1;
 lean_object* l_Lean_mkConst(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_printQuot___boxed(lean_object*);
 lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkHeader_match__2(lean_object*);
+extern lean_object* l_Lean_Meta_forallTelescopeCompatibleAux___rarg___closed__8;
 lean_object* l_Lean_Elab_log___at_Lean_Elab_Command_withLogging___spec__3(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_Modifiers_hasFormat___closed__4;
 lean_object* l_Lean_Elab_getBetterRef(lean_object*, lean_object*);
@ -211,7 +211,7 @@ x_6 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_throwUnknownId___closed__
 x_7 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_7, 0, x_6);
 lean_ctor_set(x_7, 1, x_5);
-x_8 = l_Lean_Elab_syntaxNodeKindOfAttrParam___closed__6;
+x_8 = l_Lean_Meta_forallTelescopeCompatibleAux___rarg___closed__8;
 x_9 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_9, 0, x_7);
 lean_ctor_set(x_9, 1, x_8);
@ -3617,7 +3617,7 @@ if (x_13 == 0)
 lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; uint8_t x_25; lean_object* x_26; 
 x_14 = lean_alloc_ctor(4, 1, 0);
 lean_ctor_set(x_14, 0, x_1);
-x_15 = l_Lean_Elab_syntaxNodeKindOfAttrParam___closed__6;
+x_15 = l_Lean_Meta_forallTelescopeCompatibleAux___rarg___closed__8;
 x_16 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_16, 0, x_15);
 lean_ctor_set(x_16, 1, x_14);
@ -3633,7 +3633,7 @@ lean_dec(x_20);
 x_22 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_22, 0, x_18);
 lean_ctor_set(x_22, 1, x_21);
-x_23 = l_Lean_Elab_Term_reportUnsolvedGoals___closed__3;
+x_23 = l_Lean_Meta_forallTelescopeCompatibleAux___rarg___closed__13;
 x_24 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_24, 0, x_22);
 lean_ctor_set(x_24, 1, x_23);
@ -3647,7 +3647,7 @@ lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean
 lean_dec(x_12);
 x_27 = lean_alloc_ctor(4, 1, 0);
 lean_ctor_set(x_27, 0, x_1);
-x_28 = l_Lean_Elab_syntaxNodeKindOfAttrParam___closed__6;
+x_28 = l_Lean_Meta_forallTelescopeCompatibleAux___rarg___closed__8;
 x_29 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_29, 0, x_28);
 lean_ctor_set(x_29, 1, x_27);
--- a/stage0/stdlib/Lean/Elab/Structure.c
+++ b/stage0/stdlib/Lean/Elab/Structure.c
@ -21,6 +21,7 @@ lean_object* l_Lean_Elab_Command_elabStructure___lambda__1___boxed(lean_object**
 lean_object* l_Lean_Elab_elabAttrs___at___private_Lean_Elab_Structure_2__expandCtor___spec__3(lean_object*, lean_object*, lean_object*, 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_Lean_Elab_applyVisibility___at_Lean_Elab_Command_expandDeclId___spec__5(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
+size_t l_USize_add(size_t, size_t);
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_31__elabStructureView___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_mk_cases_on(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_6__findFieldInfo_x3f___boxed(lean_object*, lean_object*);
@ -42,6 +43,7 @@ lean_object* l_Lean_Elab_Command_liftTermElabM___rarg(lean_object*, lean_object*
 lean_object* l_Lean_Syntax_getOptional_x3f(lean_object*);
 lean_object* l___private_Lean_Elab_Structure_11__withFields___main(lean_object*);
 lean_object* l___private_Lean_Elab_Structure_9__withParents___main___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_array_uget(lean_object*, size_t);
 lean_object* l___private_Lean_Elab_Structure_29__mkAuxConstructions___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_io_error_to_string(lean_object*);
 lean_object* l___private_Lean_Elab_Structure_11__withFields___main___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*);
@ -72,7 +74,6 @@ lean_object* lean_st_ref_get(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_9__withParents___main___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*);
 extern lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__11;
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_3__expandFields___spec__2___closed__12;
-extern lean_object* l_Lean_MessageData_arrayExpr_toMessageData___main___closed__1;
 lean_object* l___private_Lean_Elab_Structure_15__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_Term_ensureNoUnassignedMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkId___at___private_Lean_Elab_Structure_30__addDefaults___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -104,6 +105,7 @@ lean_object* l_Lean_Elab_Command_elabStructure___closed__10;
 lean_object* l___private_Lean_Elab_Structure_20__collectUniversesFromFields(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_3__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*);
 lean_object* l___private_Lean_Elab_Structure_11__withFields(lean_object*);
+uint8_t l_USize_decLt(size_t, size_t);
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_31__elabStructureView___spec__9(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_4__validStructType___boxed(lean_object*);
 lean_object* l___private_Lean_Elab_Structure_14__removeUnused(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -176,7 +178,6 @@ lean_object* l_Lean_Meta_mkAuxDefinition___at___private_Lean_Elab_Structure_30__
 lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_replaceRef(lean_object*, lean_object*);
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
-lean_object* l_Array_foldlStepMAux___main___at___private_Lean_Elab_Structure_2__expandCtor___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_25__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___private_Lean_Elab_Structure_11__withFields___main___rarg___closed__7;
 lean_object* l_Lean_Elab_Command_StructFieldInfo_inhabited___closed__1;
@ -255,6 +256,7 @@ lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_3__ex
 lean_object* l_Array_filterAux___main___at___private_Lean_Elab_Structure_31__elabStructureView___spec__1(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__1;
 lean_object* l___private_Lean_Elab_Structure_11__withFields___main___rarg___closed__3;
+size_t lean_usize_of_nat(lean_object*);
 extern lean_object* l_Lean_registerClassAttr___closed__2;
 lean_object* l_Lean_LocalContext_updateBinderInfo(lean_object*, lean_object*, uint8_t);
 extern lean_object* l_Lean_Elab_elabModifiers___rarg___closed__3;
@ -316,6 +318,7 @@ lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_3__ex
 lean_object* l_Lean_Elab_Command_elabStructure___closed__1;
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_3__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_Array_filterAux___main___at___private_Lean_Elab_Structure_31__elabStructureView___spec__7(lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_2__expandCtor___spec__5(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_addGlobalInstance___at___private_Lean_Elab_Structure_31__elabStructureView___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_5__checkParentIsStructure___closed__6;
 lean_object* l_Lean_Meta_mkLambdaFVars___at___private_Lean_Elab_Term_19__elabImplicitLambdaAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -333,6 +336,7 @@ lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_3__ex
 lean_object* l___private_Lean_Elab_Structure_11__withFields___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_Term_elabType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
+lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_2__expandCtor___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_8__processSubfields___main___rarg___closed__6;
 lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_3__expandFields___spec__2___closed__5;
 lean_object* l_Lean_mkForall(lean_object*, uint8_t, lean_object*, lean_object*);
@ -386,11 +390,9 @@ lean_object* l___private_Lean_Elab_Structure_17__levelMVarToParamFVars(lean_obje
 uint8_t l_Lean_Elab_Modifiers_isPrivate(lean_object*);
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 lean_object* l_Lean_Name_appendBefore(lean_object*, lean_object*);
-lean_object* l_Array_foldlStepMAux___main___at___private_Lean_Elab_Structure_2__expandCtor___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_11__withFields___main___rarg___closed__2;
 extern lean_object* l_Lean_mkOptionalNode___closed__2;
 lean_object* l___private_Lean_Elab_Structure_26__mkCtor___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l_Lean_Elab_elabAttr___rarg___lambda__2___closed__3;
 lean_object* l_Lean_Expr_inferImplicit___main(lean_object*, lean_object*, uint8_t);
 lean_object* l_Lean_Elab_elabModifiers___at___private_Lean_Elab_Structure_2__expandCtor___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Structure_28__addProjections(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -427,6 +429,7 @@ lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Structure_31__e
 lean_object* l_Lean_Elab_elabModifiers___at___private_Lean_Elab_Structure_2__expandCtor___spec__1___closed__4;
 lean_object* l_Lean_Elab_Command_checkValidFieldModifier(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Elab_Term_20__elabImplicitLambda___main___spec__1___rarg(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_Lean_Elab_elabAttr___rarg___lambda__5___closed__2;
 lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_checkValidInductiveModifier(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkConst(lean_object*, lean_object*);
@ -434,6 +437,7 @@ lean_object* l___private_Lean_Elab_Structure_11__withFields___main___rarg___clos
 lean_object* l_Lean_CollectLevelParams_main___main(lean_object*, lean_object*);
 lean_object* l_Array_forMAux___main___at___private_Lean_Elab_Structure_30__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_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*);
+extern lean_object* l_Lean_Elab_elabAttr___rarg___lambda__5___closed__3;
 lean_object* l_Array_findMAux___main___at___private_Lean_Elab_Structure_6__findFieldInfo_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_checkValidFieldModifier___closed__6;
 uint8_t lean_is_class(lean_object*, lean_object*);
@ -673,11 +677,11 @@ lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean
 lean_free_object(x_36);
 x_42 = lean_alloc_ctor(4, 1, 0);
 lean_ctor_set(x_42, 0, x_35);
-x_43 = l_Lean_Elab_elabAttr___rarg___lambda__2___closed__3;
+x_43 = l_Lean_Elab_elabAttr___rarg___lambda__5___closed__2;
 x_44 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_44, 0, x_43);
 lean_ctor_set(x_44, 1, x_42);
-x_45 = l_Lean_MessageData_arrayExpr_toMessageData___main___closed__1;
+x_45 = l_Lean_Elab_elabAttr___rarg___lambda__5___closed__3;
 x_46 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_46, 0, x_44);
 lean_ctor_set(x_46, 1, x_45);
@ -750,11 +754,11 @@ if (x_62 == 0)
 lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; 
 x_63 = lean_alloc_ctor(4, 1, 0);
 lean_ctor_set(x_63, 0, x_35);
-x_64 = l_Lean_Elab_elabAttr___rarg___lambda__2___closed__3;
+x_64 = l_Lean_Elab_elabAttr___rarg___lambda__5___closed__2;
 x_65 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_65, 0, x_64);
 lean_ctor_set(x_65, 1, x_63);
-x_66 = l_Lean_MessageData_arrayExpr_toMessageData___main___closed__1;
+x_66 = l_Lean_Elab_elabAttr___rarg___lambda__5___closed__3;
 x_67 = lean_alloc_ctor(10, 2, 0);
 lean_ctor_set(x_67, 0, x_65);
 lean_ctor_set(x_67, 1, x_66);
@ -818,44 +822,41 @@ return x_81;
 }
 }
 }
-lean_object* l_Array_foldlStepMAux___main___at___private_Lean_Elab_Structure_2__expandCtor___spec__5(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_2__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:
 {
-lean_object* x_8; uint8_t x_9; 
-x_8 = lean_array_get_size(x_2);
-x_9 = lean_nat_dec_lt(x_3, x_8);
-lean_dec(x_8);
-if (x_9 == 0)
+uint8_t x_8; 
+x_8 = x_3 < x_2;
+if (x_8 == 0)
 {
-lean_object* x_10; 
+lean_object* x_9; 
 lean_dec(x_5);
-lean_dec(x_3);
-x_10 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_10, 0, x_4);
-lean_ctor_set(x_10, 1, x_7);
-return x_10;
+x_9 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_9, 0, x_4);
+lean_ctor_set(x_9, 1, x_7);
+return x_9;
 }
 else
 {
-lean_object* x_11; lean_object* x_12; 
-x_11 = lean_array_fget(x_2, x_3);
+lean_object* x_10; lean_object* x_11; 
+x_10 = lean_array_uget(x_1, x_3);
 lean_inc(x_5);
-x_12 = l_Lean_Elab_elabAttr___at___private_Lean_Elab_Structure_2__expandCtor___spec__4(x_11, x_5, x_6, x_7);
-lean_dec(x_11);
-if (lean_obj_tag(x_12) == 0)
+x_11 = l_Lean_Elab_elabAttr___at___private_Lean_Elab_Structure_2__expandCtor___spec__4(x_10, x_5, x_6, x_7);
+lean_dec(x_10);
+if (lean_obj_tag(x_11) == 0)
 {
-lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; 
-x_13 = lean_ctor_get(x_12, 0);
+lean_object* x_12; lean_object* x_13; lean_object* x_14; size_t x_15; size_t x_16; 
+x_12 = lean_ctor_get(x_11, 0);
+lean_inc(x_12);
+x_13 = lean_ctor_get(x_11, 1);
 lean_inc(x_13);
-x_14 = lean_ctor_get(x_12, 1);
-lean_inc(x_14);
-lean_dec(x_12);
-x_15 = lean_array_push(x_4, x_13);
-x_16 = lean_nat_add(x_3, x_1);
-lean_dec(x_3);
+lean_dec(x_11);
+x_14 = lean_array_push(x_4, x_12);
+x_15 = 1;
+x_16 = x_3 + x_15;
 x_3 = x_16;
-x_4 = x_15;
-x_7 = x_14;
+x_4 = x_14;
+x_7 = x_13;
 goto _start;
 }
 else
@ -863,20 +864,19 @@ else
 uint8_t x_18; 
 lean_dec(x_5);
 lean_dec(x_4);
-lean_dec(x_3);
-x_18 = !lean_is_exclusive(x_12);
+x_18 = !lean_is_exclusive(x_11);
 if (x_18 == 0)
 {
-return x_12;
+return x_11;
 }
 else
 {
 lean_object* x_19; lean_object* x_20; lean_object* x_21; 
-x_19 = lean_ctor_get(x_12, 0);
-x_20 = lean_ctor_get(x_12, 1);
+x_19 = lean_ctor_get(x_11, 0);
+x_20 = lean_ctor_get(x_11, 1);
 lean_inc(x_20);
 lean_inc(x_19);
-lean_dec(x_12);
+lean_dec(x_11);
 x_21 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_21, 0, x_19);
 lean_ctor_set(x_21, 1, x_20);
@ -889,14 +889,59 @@ return x_21;
 lean_object* l_Lean_Elab_elabAttrs___at___private_Lean_Elab_Structure_2__expandCtor___spec__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
-lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; 
-x_5 = l_Lean_Syntax_getArgs(x_1);
-x_6 = lean_unsigned_to_nat(2u);
-x_7 = lean_unsigned_to_nat(0u);
-x_8 = l_Array_empty___closed__1;
-x_9 = l_Array_foldlStepMAux___main___at___private_Lean_Elab_Structure_2__expandCtor___spec__5(x_6, x_5, x_7, x_8, x_2, x_3, x_4);
+lean_object* x_5; lean_object* x_6; size_t x_7; size_t x_8; lean_object* x_9; lean_object* x_10; 
+x_5 = l_Lean_Syntax_getSepArgs(x_1);
+x_6 = lean_array_get_size(x_5);
+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_2__expandCtor___spec__5(x_5, x_7, x_8, x_9, x_2, x_3, x_4);
 lean_dec(x_5);
-return x_9;
+if (lean_obj_tag(x_10) == 0)
+{
+uint8_t x_11; 
+x_11 = !lean_is_exclusive(x_10);
+if (x_11 == 0)
+{
+return x_10;
+}
+else
+{
+lean_object* x_12; lean_object* x_13; lean_object* x_14; 
+x_12 = lean_ctor_get(x_10, 0);
+x_13 = lean_ctor_get(x_10, 1);
+lean_inc(x_13);
+lean_inc(x_12);
+lean_dec(x_10);
+x_14 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_14, 0, x_12);
+lean_ctor_set(x_14, 1, x_13);
+return x_14;
+}
+}
+else
+{
+uint8_t x_15; 
+x_15 = !lean_is_exclusive(x_10);
+if (x_15 == 0)
+{
+return x_10;
+}
+else
+{
+lean_object* x_16; lean_object* x_17; lean_object* x_18; 
+x_16 = lean_ctor_get(x_10, 0);
+x_17 = lean_ctor_get(x_10, 1);
+lean_inc(x_17);
+lean_inc(x_16);
+lean_dec(x_10);
+x_18 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_18, 0, x_16);
+lean_ctor_set(x_18, 1, x_17);
+return x_18;
+}
+}
 }
 }
 lean_object* l_Lean_Elab_elabDeclAttrs___at___private_Lean_Elab_Structure_2__expandCtor___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
@ -7102,15 +7147,18 @@ lean_dec(x_1);
 return x_5;
 }
 }
-lean_object* l_Array_foldlStepMAux___main___at___private_Lean_Elab_Structure_2__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) {
+lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_2__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:
 {
-lean_object* x_8; 
-x_8 = l_Array_foldlStepMAux___main___at___private_Lean_Elab_Structure_2__expandCtor___spec__5(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
-lean_dec(x_6);
+size_t x_8; size_t x_9; lean_object* x_10; 
+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_2__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_8;
+return x_10;
 }
 }
 lean_object* l_Lean_Elab_elabAttrs___at___private_Lean_Elab_Structure_2__expandCtor___spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
--- a/stage0/stdlib/Lean/Elab/Syntax.c
+++ b/stage0/stdlib/Lean/Elab/Syntax.c
--- a/stage0/stdlib/Lean/Elab/Tactic/Generalize.c
+++ b/stage0/stdlib/Lean/Elab/Tactic/Generalize.c
@ -22,7 +22,6 @@ lean_object* l_Lean_Elab_Tactic_evalGeneralizeAux_match__1(lean_object*);
 lean_object* l___private_Lean_Elab_Tactic_Generalize_0__Lean_Elab_Tactic_evalGeneralizeWithEq___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*);
 extern lean_object* l_Lean_withIncRecDepth___rarg___lambda__2___closed__2;
 lean_object* l___private_Lean_Elab_Tactic_Generalize_0__Lean_Elab_Tactic_evalGeneralizeWithEq___lambda__1___closed__1;
-lean_object* l_Lean_Syntax_getIdAt(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Tactic_Generalize_0__Lean_Elab_Tactic_evalGeneralizeWithEq_match__1(lean_object*);
 lean_object* l___private_Lean_Elab_Tactic_Generalize_0__Lean_Elab_Tactic_evalGeneralizeWithEq___lambda__1___closed__3;
 lean_object* l_Lean_Elab_Tactic_evalGeneralizeAux___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*);
@ -51,6 +50,7 @@ lean_object* lean_st_ref_take(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_assignExprMVar___at___private_Lean_Elab_Tactic_Generalize_0__Lean_Elab_Tactic_evalGeneralizeFinalize___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_throwError___at___private_Lean_Elab_Tactic_Generalize_0__Lean_Elab_Tactic_evalGeneralizeWithEq___spec__2(lean_object*);
 extern lean_object* l_Lean_Meta_inferTypeRef;
+lean_object* l_Lean_Syntax_getId(lean_object*);
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_generalize(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Tactic_evalGeneralizeAux___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -107,20 +107,22 @@ x_3 = l_Lean_Syntax_getArg(x_1, x_2);
 x_4 = l_Lean_Syntax_isNone(x_3);
 if (x_4 == 0)
 {
-lean_object* x_5; lean_object* x_6; lean_object* x_7; 
+lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; 
 x_5 = lean_unsigned_to_nat(0u);
-x_6 = l_Lean_Syntax_getIdAt(x_3, x_5);
+x_6 = l_Lean_Syntax_getArg(x_3, x_5);
 lean_dec(x_3);
-x_7 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_7, 0, x_6);
-return x_7;
+x_7 = l_Lean_Syntax_getId(x_6);
+lean_dec(x_6);
+x_8 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_8, 0, x_7);
+return x_8;
 }
 else
 {
-lean_object* x_8; 
+lean_object* x_9; 
 lean_dec(x_3);
-x_8 = lean_box(0);
-return x_8;
+x_9 = lean_box(0);
+return x_9;
 }
 }
 }
@ -136,10 +138,12 @@ return x_2;
 lean_object* l___private_Lean_Elab_Tactic_Generalize_0__Lean_Elab_Tactic_getVarName(lean_object* x_1) {
 _start:
 {
-lean_object* x_2; lean_object* x_3; 
+lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_2 = lean_unsigned_to_nat(4u);
-x_3 = l_Lean_Syntax_getIdAt(x_1, x_2);
-return x_3;
+x_3 = l_Lean_Syntax_getArg(x_1, x_2);
+x_4 = l_Lean_Syntax_getId(x_3);
+lean_dec(x_3);
+return x_4;
 }
 }
 lean_object* l___private_Lean_Elab_Tactic_Generalize_0__Lean_Elab_Tactic_getVarName___boxed(lean_object* x_1) {
@ -1887,36 +1891,35 @@ return x_12;
 lean_object* l_Lean_Elab_Tactic_evalGeneralize(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) {
 _start:
 {
-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; lean_object* x_18; 
+lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17; 
 x_11 = l___private_Lean_Elab_Tactic_Generalize_0__Lean_Elab_Tactic_getAuxHypothesisName(x_1);
-x_12 = lean_unsigned_to_nat(4u);
-x_13 = l_Lean_Syntax_getIdAt(x_1, x_12);
-x_14 = lean_unsigned_to_nat(2u);
-x_15 = l_Lean_Syntax_getArg(x_1, x_14);
-x_16 = lean_box(0);
-x_17 = 0;
+x_12 = l___private_Lean_Elab_Tactic_Generalize_0__Lean_Elab_Tactic_getVarName(x_1);
+x_13 = lean_unsigned_to_nat(2u);
+x_14 = l_Lean_Syntax_getArg(x_1, x_13);
+x_15 = lean_box(0);
+x_16 = 0;
 lean_inc(x_9);
 lean_inc(x_8);
 lean_inc(x_7);
 lean_inc(x_6);
 lean_inc(x_5);
 lean_inc(x_4);
-x_18 = l_Lean_Elab_Tactic_elabTerm(x_15, x_16, x_17, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
-if (lean_obj_tag(x_18) == 0)
+x_17 = l_Lean_Elab_Tactic_elabTerm(x_14, x_15, x_16, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
+if (lean_obj_tag(x_17) == 0)
 {
-lean_object* x_19; lean_object* x_20; lean_object* x_21; 
-x_19 = lean_ctor_get(x_18, 0);
+lean_object* x_18; lean_object* x_19; lean_object* x_20; 
+x_18 = lean_ctor_get(x_17, 0);
+lean_inc(x_18);
+x_19 = lean_ctor_get(x_17, 1);
 lean_inc(x_19);
-x_20 = lean_ctor_get(x_18, 1);
-lean_inc(x_20);
-lean_dec(x_18);
-x_21 = l_Lean_Elab_Tactic_evalGeneralizeAux(x_11, x_19, x_13, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_20);
-return x_21;
+lean_dec(x_17);
+x_20 = l_Lean_Elab_Tactic_evalGeneralizeAux(x_11, x_18, x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_19);
+return x_20;
 }
 else
 {
-uint8_t x_22; 
-lean_dec(x_13);
+uint8_t x_21; 
+lean_dec(x_12);
 lean_dec(x_11);
 lean_dec(x_9);
 lean_dec(x_8);
@ -1926,23 +1929,23 @@ lean_dec(x_5);
 lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
-x_22 = !lean_is_exclusive(x_18);
-if (x_22 == 0)
+x_21 = !lean_is_exclusive(x_17);
+if (x_21 == 0)
 {
-return x_18;
+return x_17;
 }
 else
 {
-lean_object* x_23; lean_object* x_24; lean_object* x_25; 
-x_23 = lean_ctor_get(x_18, 0);
-x_24 = lean_ctor_get(x_18, 1);
-lean_inc(x_24);
+lean_object* x_22; lean_object* x_23; lean_object* x_24; 
+x_22 = lean_ctor_get(x_17, 0);
+x_23 = lean_ctor_get(x_17, 1);
 lean_inc(x_23);
-lean_dec(x_18);
-x_25 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_25, 0, x_23);
-lean_ctor_set(x_25, 1, x_24);
-return x_25;
+lean_inc(x_22);
+lean_dec(x_17);
+x_24 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_24, 0, x_22);
+lean_ctor_set(x_24, 1, x_23);
+return x_24;
 }
 }
 }
--- a/stage0/stdlib/Lean/Elab/Tactic/Induction.c
+++ b/stage0/stdlib/Lean/Elab/Tactic/Induction.c
@ -354,19 +354,21 @@ lean_dec(x_3);
 x_6 = l_Lean_Syntax_isNone(x_5);
 if (x_6 == 0)
 {
-lean_object* x_7; lean_object* x_8; 
-x_7 = l_Lean_Syntax_getIdAt(x_5, x_4);
+lean_object* x_7; lean_object* x_8; lean_object* x_9; 
+x_7 = l_Lean_Syntax_getArg(x_5, x_4);
 lean_dec(x_5);
-x_8 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_8, 0, x_7);
-return x_8;
+x_8 = l_Lean_Syntax_getId(x_7);
+lean_dec(x_7);
+x_9 = lean_alloc_ctor(1, 1, 0);
+lean_ctor_set(x_9, 0, x_8);
+return x_9;
 }
 else
 {
-lean_object* x_9; 
+lean_object* x_10; 
 lean_dec(x_5);
-x_9 = lean_box(0);
-return x_9;
+x_10 = lean_box(0);
+return x_10;
 }
 }
 }