chore: fix codebase and tests

src/Init/Classical.lean

@@ -7,7 +7,7 @@ prelude
 import Init.Core
 import Init.NotationExtra
 
-universes u v
+universe u v
 
 /- Classical reasoning support -/
 

src/Init/Coe.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Core
 
-universes u v w w'
+universe u v w w'
 
 class Coe (α : Sort u) (β : Sort v) where
   coe : α → β

src/Init/Control/Basic.lean

@@ -6,7 +6,7 @@ Author: Leonardo de Moura, Sebastian Ullrich
 prelude
 import Init.Core
 
-universes u v w
+universe u v w
 
 @[reducible] def Functor.mapRev {f : Type u → Type v} [Functor f] {α β : Type u} : f α → (α → β) → f β :=
   fun a f => f <$> a

src/Init/Control/EState.lean

@@ -7,7 +7,7 @@ prelude
 import Init.Control.State
 import Init.Control.Except
 import Init.Data.ToString.Basic
-universes u v
+universe u v
 
 namespace EStateM
 

src/Init/Control/Option.lean

@@ -8,7 +8,7 @@ import Init.Data.Option.Basic
 import Init.Control.Basic
 import Init.Control.Except
 
-universes u v
+universe u v
 
 instance {α} : ToBool (Option α) := ⟨Option.toBool⟩
 

src/Init/Control/State.lean

@@ -9,7 +9,7 @@ prelude
 import Init.Control.Basic
 import Init.Control.Id
 import Init.Control.Except
-universes u v w
+universe u v w
 
 def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
   σ → m (α × σ)

src/Init/Core.lean

@@ -9,7 +9,7 @@ prelude
 import Init.Prelude
 import Init.SizeOf
 
-universes u v w
+universe u v w
 
 def inline {α : Sort u} (a : α) : α := a
 
@@ -824,7 +824,7 @@ protected abbrev hrecOn
 end
 
 section
-universes uA uB uC
+universe uA uB uC
 variable {α : Sort uA} {β : Sort uB} {φ : Sort uC}
 variable [s₁ : Setoid α] [s₂ : Setoid β]
 
@@ -905,7 +905,7 @@ theorem exact [s : Setoid α] {a b : α} : Quotient.mk a = Quotient.mk b → a
 end Exact
 
 section
-universes uA uB uC
+universe uA uB uC
 variable {α : Sort uA} {β : Sort uB}
 variable [s₁ : Setoid α] [s₂ : Setoid β]
 

src/Init/Data/Array/Basic.lean

@@ -10,7 +10,7 @@ import Init.Data.UInt
 import Init.Data.Repr
 import Init.Data.ToString.Basic
 import Init.Util
-universes u v w
+universe u v w
 
 namespace Array
 variable {α : Type u}

src/Init/Data/Array/BinSearch.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Array.Basic
-universes u v
+universe u v
 
 -- TODO: CLEANUP
 

src/Init/Data/Array/Subarray.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Array.Basic
 
-universes u v w
+universe u v w
 
 structure Subarray (α : Type u)  where
   as : Array α

src/Init/Data/ByteArray/Basic.lean

@@ -8,7 +8,7 @@ import Init.Data.Array.Basic
 import Init.Data.Array.Subarray
 import Init.Data.UInt
 import Init.Data.Option.Basic
-universes u
+universe u
 
 structure ByteArray where
   data : Array UInt8

src/Init/Data/FloatArray/Basic.lean

@@ -7,7 +7,7 @@ prelude
 import Init.Data.Array.Basic
 import Init.Data.Float
 import Init.Data.Option.Basic
-universes u
+universe u
 
 structure FloatArray where
   data : Array Float

src/Init/Data/Hashable.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.UInt
 import Init.Data.String
-universes u
+universe u
 
 instance : Hashable Nat where
   hash n := UInt64.ofNat n

src/Init/Data/List/Basic.lean

@@ -8,7 +8,7 @@ import Init.SimpLemmas
 import Init.Data.Nat.Basic
 open Decidable List
 
-universes u v w
+universe u v w
 
 variable {α : Type u} {β : Type v} {γ : Type w}
 

src/Init/Data/List/BasicAux.lean

@@ -7,7 +7,7 @@ prelude
 import Init.Data.List.Basic
 import Init.Util
 
-universes u
+universe u
 
 namespace List
 /- The following functions can't be defined at `Init.Data.List.Basic`, because they depend on `Init.Util`,

src/Init/Data/List/Control.lean

@@ -8,7 +8,7 @@ import Init.Control.Basic
 import Init.Data.List.Basic
 
 namespace List
-universes u v w u₁ u₂
+universe u v w u₁ u₂
 
 /-
 Remark: we can define `mapM`, `mapM₂` and `forM` using `Applicative` instead of `Monad`.

src/Init/Data/Nat/Basic.lean

@@ -5,7 +5,7 @@ Authors: Floris van Doorn, Leonardo de Moura
 -/
 prelude
 import Init.SimpLemmas
-universes u
+universe u
 
 namespace Nat
 

src/Init/Data/Nat/Control.lean

@@ -8,7 +8,7 @@ import Init.Control.Basic
 import Init.Data.Nat.Basic
 
 namespace Nat
-universes u v
+universe u v
 
 @[inline] def forM {m} [Monad m] (n : Nat) (f : Nat → m Unit) : m Unit :=
   let rec @[specialize] loop

src/Init/Data/Option/BasicAux.lean

@@ -7,7 +7,7 @@ prelude
 import Init.Data.Option.Basic
 import Init.Util
 
-universes u
+universe u
 
 namespace Option
 

src/Init/Data/Option/Instances.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Option.Basic
 
-universes u v
+universe u v
 
 theorem Option.eqOfEqSome {α : Type u} : ∀ {x y : Option α}, (∀z, x = some z ↔ y = some z) → x = y
   | none,   none,   h => rfl

src/Init/Data/Random.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.System.IO
 import Init.Data.Int
-universes u
+universe u
 
 /-
 Basic random number generator support based on the one

src/Init/Data/Range.lean

@@ -15,7 +15,7 @@ structure Range where
   step  : Nat := 1
 
 namespace Range
-universes u v
+universe u v
 
 @[inline] protected def forIn {β : Type u} {m : Type u → Type v} [Monad m] (range : Range) (init : β) (f : Nat → β → m (ForInStep β)) : m β :=
   let rec @[specialize] loop (i : Nat) (j : Nat) (b : β) : m β := do

src/Init/Data/String/Basic.lean

@@ -7,7 +7,7 @@ prelude
 import Init.Data.List.Basic
 import Init.Data.Char.Basic
 import Init.Data.Option.Basic
-universes u
+universe u
 
 def List.asString (s : List Char) : String :=
   ⟨s⟩

src/Init/Prelude.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 
-universes u v w
+universe u v w
 
 @[inline] def id {α : Sort u} (a : α) : α := a
 

src/Init/Util.lean

@@ -7,7 +7,7 @@ prelude
 import Init.Data.String.Basic
 import Init.Data.ToString.Basic
 
-universes u v
+universe u v
 /- debugging helper functions -/
 @[neverExtract, extern "lean_dbg_trace"]
 def dbgTrace {α : Type u} (s : String) (f : Unit → α) : α := f ()

src/Init/WF.lean

@@ -7,7 +7,7 @@ prelude
 import Init.SizeOf
 import Init.Data.Nat.Basic
 
-universes u v
+universe u v
 
 set_option codegen false
 

src/Lean/Data/Format.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 import Lean.Data.Options
-universes u v
+universe u v
 
 namespace Std
 namespace Format

src/Lean/Data/Json/FromToJson.lean

@@ -8,7 +8,7 @@ import Lean.Data.Json.Basic
 
 namespace Lean
 
-universes u
+universe u
 
 class FromJson (α : Type u) where
   fromJson? : Json → Except String α

src/Lean/Data/LOption.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-universes u
+universe u
 
 namespace Lean
 

src/Lean/Data/SMap.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Std.Data.HashMap
 import Std.Data.PersistentHashMap
-universes u v w w'
+universe u v w w'
 
 namespace Lean
 

src/Lean/Elab/Declaration.lean

@@ -185,7 +185,7 @@ private def isMutualPreambleCommand (stx : Syntax) : Bool :=
   k == `Lean.Parser.Command.variable ||
   k == `Lean.Parser.Command.variables ||
   k == `Lean.Parser.Command.universe ||
-  k == `Lean.Parser.Command.universes ||
+  k == `Lean.Parser.Command.universe ||
   k == `Lean.Parser.Command.check ||
   k == `Lean.Parser.Command.set_option ||
   k == `Lean.Parser.Command.open

src/Lean/Elab/Term.lean

@@ -511,7 +511,7 @@ def mkExplicitBinder (ident : Syntax) (type : Syntax) : Syntax :=
   The new parameter names are of the form `u_i` where `i >= nextParamIdx`.
   The method returns the updated expression and new `nextParamIdx`.
 
-  Remark: we make sure the generated parameter names do not clash with the universes at `ctx.levelNames`. -/
+  Remark: we make sure the generated parameter names do not clash with the universe at `ctx.levelNames`. -/
 def levelMVarToParam (e : Expr) (nextParamIdx : Nat := 1) : TermElabM (Expr × Nat) := do
   let mctx ← getMCtx
   let levelNames ← getLevelNames

src/Lean/LocalContext.lean

@@ -258,7 +258,7 @@ def getAt? (lctx : LocalContext) (i : Nat) : Option LocalDecl :=
   lctx.decls.get! i
 
 section
-universes u v
+universe u v
 variable {m : Type u → Type v} [Monad m]
 variable {β : Type u}
 
@@ -345,7 +345,7 @@ def mkForall (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr :=
   mkBinding false lctx xs b
 
 section
-universes u
+universe u
 variable {m : Type → Type u} [Monad m]
 
 @[inline] def anyM (lctx : LocalContext) (p : LocalDecl → m Bool) : m Bool :=

src/Lean/Meta/AppBuilder.lean

@@ -285,7 +285,7 @@ private partial def mkAppOptMAux (f : Expr) (xs : Array (Option Expr)) : Nat →
   ```
   mkAppOptM `Pure.pure #[m, none, none, a]
   ```
-  returns a `Pure.pure` application if the instance `Pure m` can be synthesized, and the universes match.
+  returns a `Pure.pure` application if the instance `Pure m` can be synthesized, and the universe match.
   Note that,
   ```
   mkAppM `Pure.pure #[a]

src/Lean/Parser/Basic.lean

@@ -1158,7 +1158,7 @@ def checkTailNoWs (prev : Syntax) : Bool :=
     been so by some unrelated code).
 
     For example, the universe `max` Function is parsed using this combinator so that
-    it can still be used as an identifier outside of universes (but registering it
+    it can still be used as an identifier outside of universe (but registering it
     as a token in a Term Syntax would not break the universe Parser). -/
 def nonReservedSymbolFnAux (sym : String) (errorMsg : String) : ParserFn := fun c s =>
   let initStackSz := s.stackSize

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -36,7 +36,7 @@ namespace Lean
 register_builtin_option pp.all : Bool := {
   defValue := false
   group    := "pp"
-  descr    := "(pretty printer) display coercions, implicit parameters, proof terms, fully qualified names, universes, " ++
+  descr    := "(pretty printer) display coercions, implicit parameters, proof terms, fully qualified names, universe, " ++
               "and disable beta reduction and notations during pretty printing"
 }
 register_builtin_option pp.notation : Bool := {
@@ -52,7 +52,7 @@ register_builtin_option pp.coercions : Bool := {
 register_builtin_option pp.universes : Bool := {
   defValue := false
   group    := "pp"
-  descr    := "(pretty printer) display universes"
+  descr    := "(pretty printer) display universe"
 }
 register_builtin_option pp.full_names : Bool := {
   defValue := false

src/Lean/Server/AsyncList.lean

@@ -8,7 +8,7 @@ import Init.System.IO
 
 namespace IO
 
-universes u v
+universe u v
 
 /-- An async IO list is like a lazy list but instead of being *unevaluated* `Thunk`s,
 lazy tails are `Task`s *being evaluated asynchronously*. A tail can signal the end

src/Std/Data/AssocList.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-universes u v w w'
+universe u v w w'
 namespace Std
 
 /- List-like type to avoid extra level of indirection -/

src/Std/Data/BinomialHeap.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 namespace Std
-universes u
+universe u
 namespace BinomialHeapImp
 
 structure HeapNodeAux (α : Type u) (h : Type u) where

src/Std/Data/DList.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 namespace Std
-universes u
+universe u
 /--
 A difference List is a Function that, given a List, returns the original
 contents of the difference List prepended to the given List.

src/Std/Data/HashMap.lean

@@ -5,7 +5,7 @@ Author: Leonardo de Moura
 -/
 import Std.Data.AssocList
 namespace Std
-universes u v w
+universe u v w
 
 def HashMapBucket (α : Type u) (β : Type v) :=
   { b : Array (AssocList α β) // b.size > 0 }

src/Std/Data/HashSet.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 namespace Std
-universes u v w
+universe u v w
 
 def HashSetBucket (α : Type u) :=
   { b : Array (List α) // b.size > 0 }

src/Std/Data/PersistentArray.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-universes u v w
+universe u v w
 
 namespace Std
 

src/Std/Data/PersistentHashMap.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 namespace Std
-universes u v w w'
+universe u v w w'
 
 namespace PersistentHashMap
 

src/Std/Data/PersistentHashSet.lean

@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 import Std.Data.PersistentHashMap
 
 namespace Std
-universes u v
+universe u v
 
 structure PersistentHashSet (α : Type u) [BEq α] [Hashable α] where
   (set : PersistentHashMap α Unit)

src/Std/Data/Queue.lean

@@ -7,7 +7,7 @@ Simple queue implemented using two lists.
 Note: this is only a temporary placeholder.
 -/
 namespace Std
-universes u v w
+universe u v w
 
 structure Queue (α : Type u) where
   eList : List α := []

src/Std/Data/RBMap.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 namespace Std
-universes u v w w'
+universe u v w w'
 
 inductive Rbcolor where
   | red | black

src/Std/Data/RBTree.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Std.Data.RBMap
 namespace Std
-universes u v w
+universe u v w
 
 def RBTree (α : Type u) (cmp : α → α → Ordering) : Type u :=
   RBMap α Unit cmp

src/Std/Data/Stack.lean

@@ -6,7 +6,7 @@ Authors: Daniel Selsam
 Simple stack API implemented using an array.
 -/
 namespace Std
-universes u v w
+universe u v w
 
 structure Stack (α : Type u) where
   vals : Array α := #[]

src/Std/ShareCommon.lean

@@ -8,7 +8,7 @@ import Std.Data.HashMap
 import Std.Data.PersistentHashMap
 import Std.Data.PersistentHashSet
 namespace Std
-universes u v
+universe u v
 
 namespace ShareCommon
 /-

tests/lean/PPRoundtrip.lean

@@ -48,7 +48,7 @@ section
   #eval checkM `(id Nat)
 end
 section
-  set_option pp.universe true
+  set_option pp.universes true
   #eval checkM `(List Nat)
   #eval checkM `(id Nat)
   #eval checkM `(Sum Nat Nat)

tests/lean/Reformat.lean.expected.out

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude 
 
-universes u v w
+universe u v w
 
 @[inline]
 def id {α : Sort u} (a : α) : α :=

tests/lean/Reformat/Input.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 
-universes u v w
+universe u v w
 
 @[inline] def id {α : Sort u} (a : α) : α := a
 

tests/lean/pplevel.lean

@@ -1,6 +1,6 @@
 universe u v w
 
-set_option pp.universe true
+set_option pp.universes true
 #check Type (max u v w)
 #check Type u
 #check @id.{max u v w}