diff --git a/src/Lean/Elab/DeclUtil.lean b/src/Lean/Elab/DeclUtil.lean
index 3163070b77..04851d8044 100644
--- a/src/Lean/Elab/DeclUtil.lean
+++ b/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
diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 9de9f9bd52..1101017977 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/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
diff --git a/src/Lean/Elab/Import.lean b/src/Lean/Elab/Import.lean
index f30c0fc972..d3fe944fbd 100644
--- a/src/Lean/Elab/Import.lean
+++ b/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