From d1ca45d83aea65fb2482c37372826dc335fa9234 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 8 Oct 2019 16:23:06 -0700
Subject: [PATCH] chore: use `#[]` instead of `Array.empty`

---
 library/Init/Data/ByteArray/Basic.lean         |  2 +-
 library/Init/Data/PersistentArray/Basic.lean   |  4 ++--
 library/Init/Data/PersistentHashMap/Basic.lean |  2 +-
 library/Init/Data/Stack/Basic.lean             |  4 ++--
 library/Init/Lean/Attributes.lean              |  8 ++++----
 library/Init/Lean/Compiler/IR/Basic.lean       |  2 +-
 library/Init/Lean/Compiler/IR/Borrow.lean      |  4 ++--
 library/Init/Lean/Compiler/IR/Boxing.lean      | 18 +++++++++---------
 library/Init/Lean/Compiler/IR/CompilerM.lean   |  4 ++--
 library/Init/Lean/Compiler/IR/EmitC.lean       |  2 +-
 .../Lean/Compiler/IR/ExpandResetReuse.lean     | 10 +++++-----
 library/Init/Lean/Compiler/IR/PushProj.lean    |  2 +-
 library/Init/Lean/Compiler/IR/RC.lean          |  2 +-
 .../Init/Lean/Compiler/IR/UnreachBranches.lean |  2 +-
 library/Init/Lean/Elaborator/Basic.lean        |  2 +-
 library/Init/Lean/Elaborator/PreTerm.lean      |  6 +++---
 library/Init/Lean/Parser/Parser.lean           |  6 +++---
 library/Init/Lean/Position.lean                |  4 ++--
 library/Init/Lean/TypeClass/Synth.lean         | 16 ++++++++--------
 19 files changed, 50 insertions(+), 50 deletions(-)

diff --git a/library/Init/Data/ByteArray/Basic.lean b/library/Init/Data/ByteArray/Basic.lean
index 215ad51341..ed2dd9147c 100644
--- a/library/Init/Data/ByteArray/Basic.lean
+++ b/library/Init/Data/ByteArray/Basic.lean
@@ -18,7 +18,7 @@ attribute [extern "lean_byte_array_data"] ByteArray.data
 namespace ByteArray
 @[extern c inline "lean_mk_empty_byte_array(#1)"]
 def mkEmpty (c : @& Nat) : ByteArray :=
-{ data := Array.empty }
+{ data := #[] }
 
 def empty : ByteArray :=
 mkEmpty 0
diff --git a/library/Init/Data/PersistentArray/Basic.lean b/library/Init/Data/PersistentArray/Basic.lean
index dacc0ee2af..a91a2d9786 100644
--- a/library/Init/Data/PersistentArray/Basic.lean
+++ b/library/Init/Data/PersistentArray/Basic.lean
@@ -13,7 +13,7 @@ inductive PersistentArrayNode (α : Type u)
 
 namespace PersistentArrayNode
 
-instance {α : Type u} : Inhabited (PersistentArrayNode α) := ⟨leaf Array.empty⟩
+instance {α : Type u} : Inhabited (PersistentArrayNode α) := ⟨leaf #[]⟩
 
 def isNode {α} : PersistentArrayNode α → Bool
 | node _ => true
@@ -122,7 +122,7 @@ if t.size <= (mul2Shift 1 (t.shift + initShift)).toNat then
     tailOff := t.size,
     .. t }
 else
-  { tail := Array.empty,
+  { tail := #[],
     root := let n := mkEmptyArray.push t.root;
             node (n.push (mkNewPath t.shift t.tail)),
     shift   := t.shift + initShift,
diff --git a/library/Init/Data/PersistentHashMap/Basic.lean b/library/Init/Data/PersistentHashMap/Basic.lean
index a924f10185..2f10174a72 100644
--- a/library/Init/Data/PersistentHashMap/Basic.lean
+++ b/library/Init/Data/PersistentHashMap/Basic.lean
@@ -21,7 +21,7 @@ inductive Node (α : Type u) (β : Type v) : Type (max u v)
 | entries   (es : Array (Entry α β Node)) : Node
 | collision (ks : Array α) (vs : Array β) (h : ks.size = vs.size) : Node
 
-instance Node.inhabited {α β} : Inhabited (Node α β) := ⟨Node.entries Array.empty⟩
+instance Node.inhabited {α β} : Inhabited (Node α β) := ⟨Node.entries #[]⟩
 
 abbrev shift         : USize  := 5
 abbrev branching     : USize  := USize.ofNat (2 ^ shift.toNat)
diff --git a/library/Init/Data/Stack/Basic.lean b/library/Init/Data/Stack/Basic.lean
index 31ae8bee98..69c6b5e9f1 100644
--- a/library/Init/Data/Stack/Basic.lean
+++ b/library/Init/Data/Stack/Basic.lean
@@ -11,14 +11,14 @@ import Init.Data.Int
 universes u v w
 
 structure Stack (α : Type u) :=
-(vals : Array α := Array.empty)
+(vals : Array α := #[])
 
 namespace Stack
 
 variable {α : Type u}
 
 def empty : Stack α :=
-{ vals := Array.empty }
+{}
 
 def isEmpty (s : Stack α) : Bool :=
 s.vals.isEmpty
diff --git a/library/Init/Lean/Attributes.lean b/library/Init/Lean/Attributes.lean
index 4ab40fa898..47a8ef8e47 100644
--- a/library/Init/Lean/Attributes.lean
+++ b/library/Init/Lean/Attributes.lean
@@ -35,7 +35,7 @@ IO.mkRef {}
 constant attributeMapRef : IO.Ref (HashMap Name AttributeImpl) := default _
 
 def mkAttributeArrayRef : IO (IO.Ref (Array AttributeImpl)) :=
-IO.mkRef Array.empty
+IO.mkRef #[]
 
 @[init mkAttributeArrayRef]
 constant attributeArrayRef : IO.Ref (Array AttributeImpl) := default _
@@ -153,7 +153,7 @@ do ext : PersistentEnvExtension Name NameSet ← registerPersistentEnvExtension
      addImportedFn   := fun _ => pure {},
      addEntryFn      := fun (s : NameSet) n => s.insert n,
      exportEntriesFn := fun es =>
-       let r : Array Name := es.fold (fun a e => a.push e) Array.empty;
+       let r : Array Name := es.fold (fun a e => a.push e) #[];
        r.qsort Name.quickLt,
      statsFn         := fun s => "tag attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
    };
@@ -201,7 +201,7 @@ do ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistent
      addImportedFn   := fun _ => pure {},
      addEntryFn      := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2,
      exportEntriesFn := fun m =>
-       let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) Array.empty;
+       let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) #[];
        r.qsort (fun a b => Name.quickLt a.1 b.1),
      statsFn         := fun s => "parametric attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
    };
@@ -259,7 +259,7 @@ do ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistent
      addImportedFn   := fun _ => pure {},
      addEntryFn      := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2,
      exportEntriesFn := fun m =>
-       let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) Array.empty;
+       let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) #[];
        r.qsort (fun a b => Name.quickLt a.1 b.1),
      statsFn         := fun s => "enumeration attribute extension" ++ Format.line ++ "number of local entries: " ++ format s.size
    };
diff --git a/library/Init/Lean/Compiler/IR/Basic.lean b/library/Init/Lean/Compiler/IR/Basic.lean
index ea6ebd6e1a..eeebdca07c 100644
--- a/library/Init/Lean/Compiler/IR/Basic.lean
+++ b/library/Init/Lean/Compiler/IR/Basic.lean
@@ -339,7 +339,7 @@ partial def flattenAux : FnBody → Array FnBody → (Array FnBody) × FnBody
   else flattenAux b.body (push r b)
 
 def FnBody.flatten (b : FnBody) : (Array FnBody) × FnBody :=
-flattenAux b Array.empty
+flattenAux b #[]
 
 partial def reshapeAux : Array FnBody → Nat → FnBody → FnBody
 | a, i, b =>
diff --git a/library/Init/Lean/Compiler/IR/Borrow.lean b/library/Init/Lean/Compiler/IR/Borrow.lean
index 6e2dc1e2e3..957012928f 100644
--- a/library/Init/Lean/Compiler/IR/Borrow.lean
+++ b/library/Init/Lean/Compiler/IR/Borrow.lean
@@ -182,8 +182,8 @@ do s ← get;
        ctx ← read;
        match findEnvDecl ctx.env fn with
        | some decl => pure decl.params
-       | none      => pure Array.empty   -- unreachable if well-formed input
-     | _ => pure Array.empty -- unreachable if well-formed input
+       | none      => pure #[]   -- unreachable if well-formed input
+     | _ => pure #[] -- unreachable if well-formed input
 
 /- For each ps[i], if ps[i] is owned, then mark xs[i] as owned. -/
 def ownArgsUsingParams (xs : Array Arg) (ps : Array Param) : M Unit :=
diff --git a/library/Init/Lean/Compiler/IR/Boxing.lean b/library/Init/Lean/Compiler/IR/Boxing.lean
index 9ceaf91be2..b2bf8a8271 100644
--- a/library/Init/Lean/Compiler/IR/Boxing.lean
+++ b/library/Init/Lean/Compiler/IR/Boxing.lean
@@ -62,7 +62,7 @@ do let ps := decl.params;
         else do
           x ← mkFresh;
           pure (newVDecls.push (FnBody.vdecl x p.ty (Expr.unbox q.x) (default _)), xs.push (Arg.var x)))
-     (Array.empty, Array.empty);
+     (#[], #[]);
    r ← mkFresh;
    let newVDecls := newVDecls.push (FnBody.vdecl r decl.resultType (Expr.fap decl.name xs) (default _));
    body ←
@@ -81,7 +81,7 @@ def mkBoxedVersion (decl : Decl) : Decl :=
 def addBoxedVersions (env : Environment) (decls : Array Decl) : Array Decl :=
 let boxedDecls := decls.foldl
   (fun (newDecls : Array Decl) decl => if requiresBoxedVersion env decl then newDecls.push (mkBoxedVersion decl) else newDecls)
-  Array.empty;
+  #[];
 decls ++ boxedDecls
 
 /- Infer scrutinee type using `case` alternatives.
@@ -120,7 +120,7 @@ structure BoxingState :=
    we use auxDeclCache to avoid creating equivalent auxiliary declarations more than once when
    processing the same IR declaration.
 -/
-(auxDecls : Array Decl := Array.empty)
+(auxDecls : Array Decl := #[])
 (auxDeclCache : AssocList FnBody Expr := AssocList.empty)
 (nextAuxId : Nat := 1)
 
@@ -143,7 +143,7 @@ def getJPParams (j : JoinPointId) : M (Array Param) :=
 do localCtx ← getLocalContext;
    match localCtx.getJPParams j with
    | some ys => pure ys
-   | none    => pure Array.empty -- unreachable, we assume the code is well formed
+   | none    => pure #[] -- unreachable, we assume the code is well formed
 def getDecl (fid : FunId) : M Decl :=
 do ctx ← read;
    match findEnvDecl' ctx.env fid ctx.decls with
@@ -159,7 +159,7 @@ adaptReader (fun (ctx : BoxingContext) => { localCtx := ctx.localCtx.addLocal x
 @[inline] def withJDecl {α : Type} (j : JoinPointId) (xs : Array Param) (v : FnBody) (k : M α) : M α :=
 adaptReader (fun (ctx : BoxingContext) => { localCtx := ctx.localCtx.addJP j xs v, .. ctx }) k
 
-/- If `x` declaration is of the form `x := Expr.lit _` or `x := Expr.fap c Array.empty`,
+/- If `x` declaration is of the form `x := Expr.lit _` or `x := Expr.fap c #[]`,
    and `x`'s type is not cheap to box (e.g., it is `UInt64), then return its value. -/
 private def isExpensiveConstantValueBoxing (x : VarId) (xType : IRType) : M (Option Expr) :=
 if !xType.isScalar then pure none -- We assume unboxing is always cheap
@@ -200,8 +200,8 @@ do optVal ← isExpensiveConstantValueBoxing x xType;
      | some v => pure v
      | none   => do
        let auxName  := ctx.f ++ ((`_boxed_const).appendIndexAfter s.nextAuxId);
-       let auxConst := Expr.fap auxName Array.empty;
-       let auxDecl  := Decl.fdecl auxName Array.empty expectedType body;
+       let auxConst := Expr.fap auxName #[];
+       let auxDecl  := Decl.fdecl auxName #[] expectedType body;
        modify $ fun s => {
         auxDecls     := s.auxDecls.push auxDecl,
         auxDeclCache := s.auxDeclCache.cons body auxConst,
@@ -225,7 +225,7 @@ match x with
 | _         => k x
 
 @[specialize] def castArgsIfNeededAux (xs : Array Arg) (typeFromIdx : Nat → IRType) : M (Array Arg × Array FnBody) :=
-xs.miterate (Array.empty, Array.empty) $ fun i (x : Arg) (r : Array Arg × Array FnBody) =>
+xs.miterate (#[], #[]) $ fun i (x : Arg) (r : Array Arg × Array FnBody) =>
   let expected := typeFromIdx i.val;
   let (xs, bs) := r;
   match x with
@@ -331,7 +331,7 @@ let decls := decls.foldl (fun (newDecls : Array Decl) (decl : Decl) =>
     let newDecl  := newDecl.elimDead;
     newDecls.push newDecl
   | d => newDecls.push d)
-  Array.empty;
+  #[];
 addBoxedVersions env decls
 
 end ExplicitBoxing
diff --git a/library/Init/Lean/Compiler/IR/CompilerM.lean b/library/Init/Lean/Compiler/IR/CompilerM.lean
index fc8ad529c3..2144ec1e82 100644
--- a/library/Init/Lean/Compiler/IR/CompilerM.lean
+++ b/library/Init/Lean/Compiler/IR/CompilerM.lean
@@ -34,7 +34,7 @@ def Log.toString (log : Log) : String :=
 log.format.pretty
 
 structure CompilerState :=
-(env : Environment) (log : Log := Array.empty)
+(env : Environment) (log : Log := #[])
 
 abbrev CompilerM := ReaderT Options (EState String CompilerState)
 
@@ -76,7 +76,7 @@ private def mkEntryArray (decls : List Decl) : Array Decl :=
 /- Remove duplicates by adding decls into a map -/
 let map : HashMap Name Decl := {};
 let map := decls.foldl (fun (map : HashMap Name Decl) decl => map.insert decl.name decl) map;
-map.fold (fun a k v => a.push v) Array.empty
+map.fold (fun a k v => a.push v) #[]
 
 def mkDeclMapExtension : IO (SimplePersistentEnvExtension Decl DeclMap) :=
 registerSimplePersistentEnvExtension {
diff --git a/library/Init/Lean/Compiler/IR/EmitC.lean b/library/Init/Lean/Compiler/IR/EmitC.lean
index caa8e7d8c3..47459f83fb 100644
--- a/library/Init/Lean/Compiler/IR/EmitC.lean
+++ b/library/Init/Lean/Compiler/IR/EmitC.lean
@@ -27,7 +27,7 @@ structure Context :=
 (modName    : Name)
 (jpMap      : JPParamsMap := {})
 (mainFn     : FunId := default _)
-(mainParams : Array Param := Array.empty)
+(mainParams : Array Param := #[])
 
 abbrev M := ReaderT Context (EState String String)
 
diff --git a/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean b/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean
index c7f321be70..8279cf757f 100644
--- a/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean
+++ b/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean
@@ -90,7 +90,7 @@ partial def eraseProjIncForAux (y : VarId) : Array FnBody → Mask → Array FnB
 /- Try to erase `inc` instructions on projections of `y` occurring in the tail of `bs`.
    Return the updated `bs` and a bit mask specifying which `inc`s have been removed. -/
 def eraseProjIncFor (n : Nat) (y : VarId) (bs : Array FnBody) : Array FnBody × Mask :=
-eraseProjIncForAux y bs (mkArray n none) Array.empty
+eraseProjIncForAux y bs (mkArray n none) #[]
 
 /- Replace `reuse x ctor ...` with `ctor ...`, and remoce `dec x` -/
 partial def reuseToCtor (x : VarId) : FnBody → FnBody
@@ -251,7 +251,7 @@ do let bOld := FnBody.vdecl x IRType.object (Expr.reset n y) b;
    let bSlow      := mkSlowPath x y mask b;
    bFast ← mkFastPath x y mask b;
    /- We only optimize recursively the fast. -/
-   bFast ← mainFn bFast Array.empty;
+   bFast ← mainFn bFast #[];
    c ← mkFresh;
    let b := FnBody.vdecl c IRType.uint8 (Expr.isShared y) (mkIf c bSlow bFast);
    pure $ reshape bs b
@@ -263,10 +263,10 @@ partial def searchAndExpand : FnBody → Array FnBody → M FnBody
   else
     searchAndExpand b (push bs d)
 | FnBody.jdecl j xs v b,   bs => do
-  v ← searchAndExpand v Array.empty;
+  v ← searchAndExpand v #[];
   searchAndExpand b (push bs (FnBody.jdecl j xs v FnBody.nil))
 | FnBody.case tid x xType alts,   bs => do
-  alts ← alts.mmap $ fun alt => alt.mmodifyBody $ fun b => searchAndExpand b Array.empty;
+  alts ← alts.mmap $ fun alt => alt.mmodifyBody $ fun b => searchAndExpand b #[];
   pure $ reshape bs (FnBody.case tid x xType alts)
 | b, bs =>
   if b.isTerminal then pure $ reshape bs b
@@ -278,7 +278,7 @@ match d with
 | (Decl.fdecl f xs t b) =>
   let m := mkProjMap d;
   let nextIdx := d.maxIndex + 1;
-  let b := (searchAndExpand b Array.empty { projMap := m }).run' nextIdx;
+  let b := (searchAndExpand b #[] { projMap := m }).run' nextIdx;
   Decl.fdecl f xs t b
 | d => d
 
diff --git a/library/Init/Lean/Compiler/IR/PushProj.lean b/library/Init/Lean/Compiler/IR/PushProj.lean
index f5e8773714..942f90fa7f 100644
--- a/library/Init/Lean/Compiler/IR/PushProj.lean
+++ b/library/Init/Lean/Compiler/IR/PushProj.lean
@@ -45,7 +45,7 @@ partial def FnBody.pushProj : FnBody → FnBody
   match term with
   | FnBody.case tid x xType alts =>
     let altsF      := alts.map $ fun alt => alt.body.freeIndices;
-    let (bs, alts) := pushProjs bs alts altsF Array.empty (mkIndexSet x.idx);
+    let (bs, alts) := pushProjs bs alts altsF #[] (mkIndexSet x.idx);
     let alts       := alts.map $ fun alt => alt.modifyBody FnBody.pushProj;
     let term       := FnBody.case tid x xType alts;
     reshape bs term
diff --git a/library/Init/Lean/Compiler/IR/RC.lean b/library/Init/Lean/Compiler/IR/RC.lean
index 8122441d44..cb68a1ee25 100644
--- a/library/Init/Lean/Compiler/IR/RC.lean
+++ b/library/Init/Lean/Compiler/IR/RC.lean
@@ -43,7 +43,7 @@ match ctx.varMap.find x with
 def getJPParams (ctx : Context) (j : JoinPointId) : Array Param :=
 match ctx.localCtx.getJPParams j with
 | some ps => ps
-| none    => Array.empty -- unreachable in well-formed code
+| none    => #[] -- unreachable in well-formed code
 
 def getJPLiveVars (ctx : Context) (j : JoinPointId) : LiveVarSet :=
 match ctx.jpLiveVarMap.find j with
diff --git a/library/Init/Lean/Compiler/IR/UnreachBranches.lean b/library/Init/Lean/Compiler/IR/UnreachBranches.lean
index 46bbb12447..f56c53844f 100644
--- a/library/Init/Lean/Compiler/IR/UnreachBranches.lean
+++ b/library/Init/Lean/Compiler/IR/UnreachBranches.lean
@@ -50,7 +50,7 @@ partial def merge : Value → Value → Value
 | top, _ => top
 | _, top => top
 | v₁@(ctor i₁ vs₁), v₂@(ctor i₂ vs₂) =>
-  if i₁ == i₂ then ctor i₁ $ vs₁.size.fold (fun i r => r.push (merge (vs₁.get! i) (vs₂.get! i))) Array.empty
+  if i₁ == i₂ then ctor i₁ $ vs₁.size.fold (fun i r => r.push (merge (vs₁.get! i) (vs₂.get! i))) #[]
   else choice [v₁, v₂]
 | choice vs₁, choice vs₂ => choice $ vs₁.foldl (addChoice merge) vs₂
 | choice vs, v => choice $ addChoice merge vs v
diff --git a/library/Init/Lean/Elaborator/Basic.lean b/library/Init/Lean/Elaborator/Basic.lean
index 1da00074c0..f23602b2be 100644
--- a/library/Init/Lean/Elaborator/Basic.lean
+++ b/library/Init/Lean/Elaborator/Basic.lean
@@ -199,7 +199,7 @@ do ext : PersistentEnvExtension ElabAttributeEntry σ ← registerPersistentEnvE
        -- TODO: populate table with `es`
        pure table,
      addEntryFn      := fun (s : σ) _ => s,                            -- TODO
-     exportEntriesFn := fun _ => Array.empty,                          -- TODO
+     exportEntriesFn := fun _ => #[],                                  -- TODO
      statsFn         := fun _ => fmt (kind ++ " elaborator attribute") -- TODO
    };
    let attrImpl : AttributeImpl := {
diff --git a/library/Init/Lean/Elaborator/PreTerm.lean b/library/Init/Lean/Elaborator/PreTerm.lean
index b164fe23ad..12376024d3 100644
--- a/library/Init/Lean/Elaborator/PreTerm.lean
+++ b/library/Init/Lean/Elaborator/PreTerm.lean
@@ -167,12 +167,12 @@ match b.getKind with
        | _ => throw "unknown binder default value annotation";
      decl ← mkLocalDecl id type;
      pure (mkLocal decl)
-| `Lean.Parser.Term.implicitBinder => do runIO (IO.println $ ">> implict " ++ (toString b)); pure Array.empty
-| `Lean.Parser.Term.instBinder     => do runIO (IO.println $ ">> inst " ++ (toString b)); pure Array.empty
+| `Lean.Parser.Term.implicitBinder => do runIO (IO.println $ ">> implict " ++ (toString b)); pure #[]
+| `Lean.Parser.Term.instBinder     => do runIO (IO.println $ ">> inst " ++ (toString b)); pure #[]
 | _ => throw "unknown binder kind"
 
 private def processBinders (bs : Array (Syntax Expr)) : Elab (Array PreTerm) :=
-bs.mfoldl (fun r s => do xs ← processBinder s; pure (r ++ xs)) Array.empty
+bs.mfoldl (fun r s => do xs ← processBinder s; pure (r ++ xs)) #[]
 
 @[builtinPreTermElab «forall»] def convertForall : PreTermElab :=
 fun n => do
diff --git a/library/Init/Lean/Parser/Parser.lean b/library/Init/Lean/Parser/Parser.lean
index c2c5ecfbd6..d1c4995fb0 100644
--- a/library/Init/Lean/Parser/Parser.lean
+++ b/library/Init/Lean/Parser/Parser.lean
@@ -114,7 +114,7 @@ match e₂ with
 end Error
 
 structure ParserState :=
-(stxStack : Array Syntax := Array.empty)
+(stxStack : Array Syntax := #[])
 (pos      : String.Pos := 0)
 (cache    : ParserCache := {})
 (errorMsg : Option Error := none)
@@ -1350,7 +1350,7 @@ do ext : PersistentEnvExtension TokenConfig TokenTable ← registerPersistentEnv
      name            := `_tokens_,
      addImportedFn   := fun es => mkImportedTokenTable es,
      addEntryFn      := fun (s : TokenTable) _ => s,         -- TODO
-     exportEntriesFn := fun _ => Array.empty,                -- TODO
+     exportEntriesFn := fun _ => #[],                        -- TODO
      statsFn         := fun _ => fmt "token table attribute" -- TODO
    };
    let attrImpl : AttributeImpl := {
@@ -1520,7 +1520,7 @@ do ext : PersistentEnvExtension ParserAttributeEntry ParsingTables ← registerP
     -- TODO: populate table with `es`
        pure table,
      addEntryFn      := fun (s : ParsingTables) _ => s, -- TODO
-     exportEntriesFn := fun _ => Array.empty,           -- TODO
+     exportEntriesFn := fun _ => #[],                   -- TODO
      statsFn         := fun _ => fmt "parser attribute" -- TODO
    };
    let attrImpl : AttributeImpl := {
diff --git a/library/Init/Lean/Position.lean b/library/Init/Lean/Position.lean
index 311f7cea05..e6f164e052 100644
--- a/library/Init/Lean/Position.lean
+++ b/library/Init/Lean/Position.lean
@@ -42,7 +42,7 @@ structure FileMap :=
 namespace FileMap
 
 instance : Inhabited FileMap :=
-⟨{ source := "", positions := Array.empty, lines := Array.empty }⟩
+⟨{ source := "", positions := #[], lines := #[] }⟩
 
 private partial def ofStringAux (s : String) : String.Pos → Nat → Array String.Pos → Array Nat → FileMap
 | i, line, ps, lines =>
@@ -54,7 +54,7 @@ private partial def ofStringAux (s : String) : String.Pos → Nat → Array Stri
     else ofStringAux i line ps lines
 
 def ofString (s : String) : FileMap :=
-ofStringAux s 0 1 (Array.empty.push 0) (Array.empty.push 1)
+ofStringAux s 0 1 (#[0]) (#[1])
 
 private partial def toColumnAux (str : String) (lineBeginPos : String.Pos) (pos : String.Pos) : String.Pos → Nat → Nat
 | i, c =>
diff --git a/library/Init/Lean/TypeClass/Synth.lean b/library/Init/Lean/TypeClass/Synth.lean
index be87699c97..672840821f 100644
--- a/library/Init/Lean/TypeClass/Synth.lean
+++ b/library/Init/Lean/TypeClass/Synth.lean
@@ -60,7 +60,7 @@ instance GeneratorNode.Inhabited : Inhabited GeneratorNode :=
 
 structure TableEntry : Type :=
 (waiters    : Array Waiter)
-(answers    : Array TypedExpr := Array.empty)
+(answers    : Array TypedExpr := #[])
 
 structure TCState : Type :=
 (env            : Environment)
@@ -134,8 +134,8 @@ partial def introduceLocals : Nat → LocalContext → Array Expr → Expr → L
 def tryResolve (ctx : Context) (futureAnswer : TypedExpr) (instTE : TypedExpr) : TCMethod (Option (Context × List Expr)) :=
 do let ⟨mvar, mvarType⟩ := futureAnswer;
    let ⟨instVal, instType⟩ := instTE;
-   let ⟨lctx, mvarType, locals⟩ := introduceLocals 0 {} Array.empty mvarType;
-   let ⟨ctx, instVal, instType, newMVars⟩ := introduceMVars lctx locals ctx instVal instType Array.empty;
+   let ⟨lctx, mvarType, locals⟩ := introduceLocals 0 {} #[] mvarType;
+   let ⟨ctx, instVal, instType, newMVars⟩ := introduceMVars lctx locals ctx instVal instType #[];
    match (Context.eUnify mvarType instType *> Context.eUnify mvar (lctx.mkLambda locals instVal)).run ctx with
    | EState.Result.error msg   _ => pure none
    | EState.Result.ok    _   ctx => pure $ some $ (ctx, newMVars.toList) -- TODO(dselsam): rm toList
@@ -269,21 +269,21 @@ def collectEReplacements (env : Environment) (lctx : LocalContext) (locals : Arr
 
 def preprocessForOutParams (env : Environment) (goalType : Expr) : Context × Expr × Array (Level × Level) × Array (Expr × Expr) :=
 if !goalType.hasMVar && goalType.getAppFn.isConst && !hasOutParams env goalType.getAppFn.constName
-then ({}, goalType, Array.empty, Array.empty)
+then ({}, goalType, #[], #[])
 else
-  let ⟨lctx, bodyGoalType, locals⟩ := introduceLocals 0 {} Array.empty goalType;
+  let ⟨lctx, bodyGoalType, locals⟩ := introduceLocals 0 {} #[] goalType;
   let f := goalType.getAppFn;
   let fArgs := goalType.getAppArgs;
   if !(f.isConst && isClass env f.constName)
-  then ({}, goalType, Array.empty, Array.empty)
+  then ({}, goalType, #[], #[])
   else
-    let ⟨ctx, uReplacements, CLevels⟩ := collectUReplacements f.constLevels {} Array.empty Array.empty;
+    let ⟨ctx, uReplacements, CLevels⟩ := collectUReplacements f.constLevels {} #[] #[];
     let f := if uReplacements.isEmpty then f else Expr.const f.constName CLevels.toList;
     let fType :=
       match env.find f.constName with
       | none => panic! "found constant not in the environment"
       | some cInfo => cInfo.instantiateTypeUnivParams CLevels.toList;
-    let (ctx, eReplacements, fArgs) := collectEReplacements env lctx locals fType fArgs ctx Array.empty Array.empty;
+    let (ctx, eReplacements, fArgs) := collectEReplacements env lctx locals fType fArgs ctx #[] #[];
     (ctx, lctx.mkForall locals $ mkApp f fArgs.toList, uReplacements, eReplacements)
 
 def synth (goalType₀ : Expr) (fuel : Nat := 100000) : TCMethod Expr :=