chore(library/init): Empty => empty when it is a function

library/init/data/array/basic.lean

@@ -40,10 +40,10 @@ def mkNil (_ : Unit) : Array α :=
 { sz   := 0,
   data := λ ⟨x, h⟩, absurd h (Nat.notLtZero x) }
 
-def nil : Array α :=
+def empty : Array α :=
 mkNil ()
 
-def Empty (a : Array α) : Bool :=
+def isEmpty (a : Array α) : Bool :=
 a.size = 0
 
 @[extern cpp inline "lean::array_read(#2, #3)"]
@@ -155,4 +155,4 @@ def List.toArrayAux {α : Type u} : List α → Array α → Array α
 | (a::as) r := List.toArrayAux as (r.push a)
 
 def List.toArray {α : Type u} (l : List α) : Array α :=
-l.toArrayAux Array.nil
+l.toArrayAux Array.empty

library/init/data/dlist.lean

@@ -23,7 +23,7 @@ open List
 def ofList (l : List α) : Dlist α :=
 ⟨append l, λ t, (appendNil l).symm ▸ rfl⟩
 
-def Empty : Dlist α :=
+def empty : Dlist α :=
 ⟨id, λ t, rfl⟩
 
 def toList : Dlist α → List α

library/init/data/hashmap/basic.lean

@@ -135,7 +135,7 @@ def size (m : DHashmap α β) : Nat :=
 match m with
 | ⟨ {size := sz, ..}, _ ⟩ := sz
 
-@[inline] def Empty (m : DHashmap α β) : Bool :=
+@[inline] def empty (m : DHashmap α β) : Bool :=
 m.size = 0
 
 end DHashmap
@@ -167,7 +167,7 @@ DHashmap.fold m d f
 @[inline] def size (m : Hashmap α β) : Nat :=
 DHashmap.size m
 
-@[inline] def Empty (m : Hashmap α β) : Bool :=
-DHashmap.Empty m
+@[inline] def empty (m : Hashmap α β) : Bool :=
+DHashmap.empty m
 
 end Hashmap

library/init/data/rbmap/basic.lean

@@ -166,7 +166,7 @@ t.val.depth f
 @[inline] def mfor {m : Type w → Type w'} [Monad m] (f : α → β → m σ) (t : RBMap α β lt) : m PUnit :=
 t.mfold (λ k v _, f k v *> pure ⟨⟩) ⟨⟩
 
-@[inline] def Empty : RBMap α β lt → Bool
+@[inline] def empty : RBMap α β lt → Bool
 | ⟨leaf, _⟩ := true
 | _         := false
 

library/init/data/rbtree/basic.lean

@@ -31,8 +31,8 @@ RBMap.mfold (λ a _ r, f a r) t b
 @[inline] def mfor {m : Type v → Type w} [Monad m] (f : α → m β) (t : RBTree α lt) : m PUnit :=
 t.mfold (λ a _, f a *> pure ⟨⟩) ⟨⟩
 
-@[inline] def Empty (t : RBTree α lt) : Bool :=
-RBMap.Empty t
+@[inline] def empty (t : RBTree α lt) : Bool :=
+RBMap.empty t
 
 @[specialize] def toList (t : RBTree α lt) : List α :=
 t.revFold (::) []

library/init/lean/elaborator.lean

@@ -66,7 +66,7 @@ structure OrderedRBMap (α β : Type) (lt : α → α → Prop) :=
 namespace OrderedRBMap
 variables {α β : Type} {lt : α → α → Prop} [DecidableRel lt] (m : OrderedRBMap α β lt)
 
-def Empty : OrderedRBMap α β lt := {entries := [], map := mkRBMap _ _ _, size := 0}
+def empty : OrderedRBMap α β lt := {entries := [], map := mkRBMap _ _ _, size := 0}
 
 def insert (k : α) (v : β) : OrderedRBMap α β lt :=
 {entries := (k, v)::m.entries, map := m.map.insert k (m.size, v), size := m.size + 1}
@@ -75,7 +75,7 @@ def find (a : α) : Option (Nat × β) :=
 m.map.find a
 
 def ofList (l : List (α × β)) : OrderedRBMap α β lt :=
-l.foldl (λ m p, OrderedRBMap.insert m (Prod.fst p) (Prod.snd p)) OrderedRBMap.Empty
+l.foldl (λ m p, OrderedRBMap.insert m (Prod.fst p) (Prod.snd p)) OrderedRBMap.empty
 end OrderedRBMap
 
 structure ElaboratorConfig extends FrontendConfig :=
@@ -93,9 +93,9 @@ structure Scope :=
 (notations : List NotationMacro := [])
 /- The set of local universe variables.
    We remember their insertion order so that we can keep the order when copying them to declarations. -/
-(univs : OrderedRBMap Name Level (<) := OrderedRBMap.Empty)
+(univs : OrderedRBMap Name Level (<) := OrderedRBMap.empty)
 /- The set of local variables. -/
-(vars : OrderedRBMap Name SectionVar (<) := OrderedRBMap.Empty)
+(vars : OrderedRBMap Name SectionVar (<) := OrderedRBMap.empty)
 /- The subset of `vars` that is tagged as always included. -/
 (includeVars : RBTree Name (<) := mkRBTree _ _)
 /- The stack of nested active `namespace` commands. -/
@@ -120,7 +120,7 @@ structure ElaboratorState :=
 
 -- Stack of current scopes. The bottom-most Scope is the Module Scope.
 (scopes : List Scope)
-(messages : MessageLog := MessageLog.Empty)
+(messages : MessageLog := MessageLog.empty)
 (parserCfg : ModuleParserConfig)
 (expanderCfg : Expander.ExpanderConfig)
 (env : environment)
@@ -988,7 +988,7 @@ def mkState (cfg : ElaboratorConfig) (env : environment) (opts : Options) : Elab
   scopes := [{cmd := "MODULE", header := `MODULE, Options := opts}]}
 
 def processCommand (cfg : ElaboratorConfig) (st : ElaboratorState) (cmd : Syntax) : ElaboratorState :=
-let st := {st with messages := MessageLog.Empty} in
+let st := {st with messages := MessageLog.empty} in
 let r := @ExceptT.run _ id _ $ flip StateT.run st $ flip ReaderT.run cfg $ RecT.run
   (command.elaborate cmd)
   (λ _, error cmd "Elaborator.run: recursion depth exceeded")

library/init/lean/message.lean

@@ -40,7 +40,7 @@ structure MessageLog :=
 (revList : List Message)
 
 namespace MessageLog
-def Empty : MessageLog :=
+def empty : MessageLog :=
 ⟨[]⟩
 
 def add (msg : Message) (log : MessageLog) : MessageLog :=

library/init/lean/parser/basic.lean

@@ -127,10 +127,10 @@ def messageOfParsecMessage {μ : Type} (cfg : FrontendConfig) (msg : Parsec.Mess
 /-- Run Parser stack, returning a partial Syntax tree in case of a fatal error -/
 protected def run {m : Type → Type} {α ρ : Type} [Monad m] [HasCoeT ρ FrontendConfig] (cfg : ρ) (s : String) (r : StateT ParserState (ParserT ρ m) α) :
 m (Sum α Syntax × MessageLog) :=
-do (r, _) ← (((r.run {messages:=MessageLog.Empty}).run cfg).parse s).run {},
+do (r, _) ← (((r.run {messages:=MessageLog.empty}).run cfg).parse s).run {},
 pure $ match r with
 | Except.ok (a, st) := (Sum.inl a, st.messages)
-| Except.error msg  := (Sum.inr msg.custom.get, MessageLog.Empty.add (messageOfParsecMessage cfg msg))
+| Except.error msg  := (Sum.inr msg.custom.get, MessageLog.empty.add (messageOfParsecMessage cfg msg))
 
 open MonadParsec
 open Parser.HasView

library/init/lean/parser/combinators.lean

@@ -69,7 +69,7 @@ instance many.tokens (r : Parser) [Parser.HasTokens r] : Parser.HasTokens (many
 ⟨tokens r⟩
 
 instance many.view (r : Parser) [HasView α r] : Parser.HasView (List α) (many r) :=
-/- Remark: `many1.view` can handle Empty List. -/
+/- Remark: `many1.view` can handle empty list. -/
 {..many1.view r}
 
 private def sepByAux (p : m Syntax) (sep : Parser) (allowTrailingSep : Bool) : Bool → List Syntax → Nat → Parser

library/init/lean/parser/module.lean

@@ -114,7 +114,7 @@ structure ModuleParserSnapshot :=
 -- return (partial) Syntax tree and single fatal or multiple non-fatal messages
 def resumeModuleParser {α : Type} (cfg : ModuleParserConfig) (snap : ModuleParserSnapshot) (mkRes : α → Syntax × ModuleParserSnapshot)
   (p : ModuleParserM α) : Syntax × Except Message (ModuleParserSnapshot × MessageLog) :=
-let (r, _) := ((((Prod.mk <$> p <*> leftOver).run {messages:=MessageLog.Empty}).run cfg).runFrom snap.it).run {} in
+let (r, _) := ((((Prod.mk <$> p <*> leftOver).run {messages:=MessageLog.empty}).run cfg).runFrom snap.it).run {} in
 match r with
 | Except.ok ((a, it), st) := let (stx, snap) := mkRes a in (stx, Except.ok ({snap with it := it}, st.messages))
 | Except.error msg  := (msg.custom.get, Except.error $ messageOfParsecMessage cfg msg)

library/init/lean/parser/parsec.lean

@@ -21,7 +21,7 @@ namespace Parsec
 structure Message (μ : Type := Unit) :=
 (it         : Iterator)
 (unexpected : String       := "")          -- unexpected input
-(expected   : Dlist String := Dlist.Empty) -- expected productions
+(expected   : Dlist String := Dlist.empty) -- expected productions
 (custom     : Option μ)
 
 def expected.toString : List String → String
@@ -59,7 +59,7 @@ inductive Result (μ α : Type)
 | error {} (msg : Message μ) (consumed : Bool)                     : Result
 
 @[inline] def Result.mkEps {μ α : Type} (a : α) (it : Iterator) : Result μ α :=
-Result.ok a it (some Dlist.Empty)
+Result.ok a it (some Dlist.empty)
 end Parsec
 
 open Parsec
@@ -259,7 +259,7 @@ namespace MonadParsec
 open ParsecT
 variables {m : Type → Type} [Monad m] [MonadParsec μ m] {α β : Type}
 
-def error {α : Type} (unexpected : String) (expected : Dlist String := Dlist.Empty)
+def error {α : Type} (unexpected : String) (expected : Dlist String := Dlist.empty)
           (it : Option Iterator := none) (custom : Option μ := none) : m α :=
 lift $ λ it', Result.error { unexpected := unexpected, expected := expected, it := it.getOrElse it', custom := custom } false
 
@@ -279,7 +279,7 @@ labels p (Dlist.singleton lbl)
 infixr ` <?> `:2 := label
 
 @[inline] def hidden (p : m α) : m α :=
-labels p Dlist.Empty
+labels p Dlist.empty
 
 /--
 `try p` behaves like `p`, but it pretends `p` hasn't
@@ -470,7 +470,7 @@ String.Iterator.offset <$> leftOver
 @[inline] def notFollowedBy [MonadExcept (Message μ) m] (p : m α) (msg : String := "input") : m Unit :=
 do it ← leftOver,
    b ← lookahead $ catch (p *> pure false) (λ _, pure true),
-   if b then pure () else error msg Dlist.Empty it
+   if b then pure () else error msg Dlist.empty it
 
 def eoi : m Unit :=
 do it ← leftOver,
@@ -534,7 +534,7 @@ def unexpected (msg : String) : m α :=
 error msg
 
 def unexpectedAt (msg : String) (it : Iterator) : m α :=
-error msg Dlist.Empty it
+error msg Dlist.empty it
 
 /- Execute all parsers in `ps` and return the Result of the longest parse(s) if any,
    or else the Result of the furthest error. If there are two parses of

tests/compiler/array_test.lean

@@ -7,7 +7,7 @@ a
 
 def main : IO UInt32 :=
 do
- let a : Array Nat := Array.nil,
+ let a : Array Nat := Array.empty,
  IO.println (toString a),
  IO.println (toString a.sz),
  let a := foo a,