diff --git a/library/Init/Lean/Compiler/IR/Basic.lean b/library/Init/Lean/Compiler/IR/Basic.lean
index fc93545bf1..ea6ebd6e1a 100644
--- a/library/Init/Lean/Compiler/IR/Basic.lean
+++ b/library/Init/Lean/Compiler/IR/Basic.lean
@@ -552,10 +552,10 @@ instance : Inhabited VarIdSet := ⟨{}⟩
 end VarIdSet
 
 def mkIf (x : VarId) (t e : FnBody) : FnBody :=
-FnBody.case `Bool x IRType.uint8 [
+FnBody.case `Bool x IRType.uint8 #[
   Alt.ctor {name := `Bool.false, cidx := 0, size := 0, usize := 0, ssize := 0} e,
   Alt.ctor {name := `Bool.true, cidx := 1, size := 0, usize := 0, ssize := 0} t
-].toArray
+]
 
 end IR
 end Lean
diff --git a/library/Init/Lean/Compiler/IR/Default.lean b/library/Init/Lean/Compiler/IR/Default.lean
index 1bbe40cb36..35b1254e9b 100644
--- a/library/Init/Lean/Compiler/IR/Default.lean
+++ b/library/Init/Lean/Compiler/IR/Default.lean
@@ -66,7 +66,7 @@ env ← getEnv;
 if !ExplicitBoxing.requiresBoxedVersion env decl then pure ()
 else do
   let decl := ExplicitBoxing.mkBoxedVersion decl;
-  let decls : Array Decl := Array.singleton decl;
+  let decls : Array Decl := #[decl];
   decls ← explicitRC decls;
   decls.mfor $ fun decl => modifyEnv $ fun env => addDeclAux env decl;
   pure ()
diff --git a/library/Init/Lean/Parser/Module.lean b/library/Init/Lean/Parser/Module.lean
index ce2d1bb2af..e716a58428 100644
--- a/library/Init/Lean/Parser/Module.lean
+++ b/library/Init/Lean/Parser/Module.lean
@@ -51,7 +51,7 @@ match s.errorMsg with
 
 private def mkEOI (pos : String.Pos) : Syntax :=
 let atom := mkAtom { pos := pos, trailing := "".toSubstring, leading := "".toSubstring } "";
-Syntax.node `Lean.Parser.Module.eoi [atom].toArray
+Syntax.node `Lean.Parser.Module.eoi #[atom]
 
 def isEOI (s : Syntax) : Bool :=
 s.isOfKind `Lean.Parser.Module.eoi
@@ -125,7 +125,7 @@ fname ← IO.realPath fname;
 contents ← IO.readTextFile fname;
 let ctx := mkParserContextCore env contents fname;
 let (stx, state, messages) := parseHeader env ctx;
-parseFileAux env ctx state messages (Array.singleton stx)
+parseFileAux env ctx state messages #[stx]
 
 end Parser
 end Lean
diff --git a/library/Init/Lean/Parser/Term.lean b/library/Init/Lean/Parser/Term.lean
index 9b14437d26..19acb9b6f4 100644
--- a/library/Init/Lean/Parser/Term.lean
+++ b/library/Init/Lean/Parser/Term.lean
@@ -177,7 +177,7 @@ def checkIsSort := checkLeading (fun leading => leading.isOfKind `Lean.Parser.Te
 end Term
 
 def mkAppStx {α} (fn : Syntax α) (args : List (Syntax α)) : Syntax α :=
-args.foldl (fun fn arg => Syntax.node `Lean.Parser.Term.app [fn, arg].toArray) fn
+args.foldl (fun fn arg => Syntax.node `Lean.Parser.Term.app #[fn, arg]) fn
 
 end Parser
 end Lean
diff --git a/library/Init/Lean/Parser/Transform.lean b/library/Init/Lean/Parser/Transform.lean
index efbfbeee20..d0bf65ae25 100644
--- a/library/Init/Lean/Parser/Transform.lean
+++ b/library/Init/Lean/Parser/Transform.lean
@@ -22,7 +22,7 @@ match stx with
     | none =>
       let newArgs := newArgs.push (atom none sepTk);
       newArgs.push arg)
-    (Array.singleton (args.get! 0))
+    #[args.get! 0]
     1;
   node k args
 | stx => stx
diff --git a/library/Init/Lean/Path.lean b/library/Init/Lean/Path.lean
index 438bd58801..f20aca7acc 100644
--- a/library/Init/Lean/Path.lean
+++ b/library/Init/Lean/Path.lean
@@ -21,7 +21,7 @@ do fname ← IO.realPath fname;
 
 def mkSearchPathRef : IO (IO.Ref (Array String)) :=
 do curr ← realPathNormalized ".";
-   IO.mkRef (Array.singleton curr)
+   IO.mkRef #[curr]
 
 @[init mkSearchPathRef]
 constant searchPathRef : IO.Ref (Array String) := default _
diff --git a/library/Init/Lean/Syntax.lean b/library/Init/Lean/Syntax.lean
index d8e6439bb8..b12c1b389b 100644
--- a/library/Init/Lean/Syntax.lean
+++ b/library/Init/Lean/Syntax.lean
@@ -353,14 +353,14 @@ Syntax.node nullKind args.toArray
 
 def mkOptionalNode {α} (arg : Option (Syntax α)) : Syntax α :=
 match arg with
-| some arg => Syntax.node nullKind (Array.singleton arg)
+| some arg => Syntax.node nullKind #[arg]
 | none     => Syntax.node nullKind Array.empty
 
 /- Helper functions for creating string and numeric literals -/
 
 def mkLit (kind : SyntaxNodeKind) (val : String) (info : Option SourceInfo := none) : Syntax :=
 let atom : Syntax := Syntax.atom info val;
-Syntax.node kind (Array.singleton atom)
+Syntax.node kind #[atom]
 
 def mkStrLit (val : String) (info : Option SourceInfo := none) : Syntax :=
 mkLit strLitKind val info
diff --git a/library/Init/Lean/TypeClass/Synth.lean b/library/Init/Lean/TypeClass/Synth.lean
index 884ca26839..44c59ca56d 100644
--- a/library/Init/Lean/TypeClass/Synth.lean
+++ b/library/Init/Lean/TypeClass/Synth.lean
@@ -103,7 +103,7 @@ do let mvarType := ctx.eInfer mvar;
        futureAnswer       := ⟨mvar, mvarType⟩,
        remainingInstances := (getClassInstances ϕ.env n).map Instance.const
      };
-     let tableEntry : TableEntry := { waiters := [waiter].toArray };
+     let tableEntry : TableEntry := { waiters := #[waiter] };
      modify $ λ ϕ => {
        generatorStack := ϕ.generatorStack.push gNode,
        tableEntries   := ϕ.tableEntries.insert gNode.anormSubgoal tableEntry,