chore: remove command universes

Now, `universe` may declare many universes. The goal is to make it
consistent with the `variable` command

src/Lean/Elab/BuiltinCommand.lean

@@ -93,9 +93,6 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
   elabChoiceAux stx.getArgs 0
 
 @[builtinCommandElab «universe»] def elabUniverse : CommandElab := fun n => do
-  addUnivLevel n[1]
-
-@[builtinCommandElab «universes»] def elabUniverses : CommandElab := fun n => do
   n[1].forArgsM addUnivLevel
 
 @[builtinCommandElab «init_quot»] def elabInitQuot : CommandElab := fun stx => do

src/Lean/Parser/Command.lean

@@ -68,8 +68,7 @@ declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant»
 @[builtinCommandParser] def «namespace»    := leading_parser "namespace " >> ident
 @[builtinCommandParser] def «end»          := leading_parser "end " >> optional ident
 @[builtinCommandParser] def «variable»     := leading_parser "variable" >> many1 Term.bracketedBinder
-@[builtinCommandParser] def «universe»     := leading_parser "universe " >> ident
-@[builtinCommandParser] def «universes»    := leading_parser "universes " >> many1 ident
+@[builtinCommandParser] def «universe»     := leading_parser "universe " >> many1 ident
 @[builtinCommandParser] def check          := leading_parser "#check " >> termParser
 @[builtinCommandParser] def check_failure  := leading_parser "#check_failure " >> termParser -- Like `#check`, but succeeds only if term does not type check
 @[builtinCommandParser] def reduce         := leading_parser "#reduce " >> termParser

tests/bench/rbmap.lean

@@ -9,7 +9,7 @@ import Init.Data.List.BasicAux
 import Init.Data.String
 import Init.System.IO
 
-universes u v w w'
+universe u v w w'
 
 inductive color
 | Red | Black

tests/bench/rbmap2.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import init.coe init.data.option.basic init.system.io
 
-universes u v w w'
+universe u v w w'
 
 inductive color
 | Red | Black

tests/bench/rbmap3.lean

@@ -1,7 +1,7 @@
 prelude
 import init.core init.system.io init.data.ordering
 
-universes u v w
+universe u v w
 
 inductive Rbcolor
 | red | black

tests/bench/rbmap4.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import init.coe init.data.option.basic init.system.io
 
-universes u v w w'
+universe u v w w'
 
 inductive color
 | Red | Black

tests/bench/rbmap500k.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import init.coe init.data.option.basic init.system.io
 
-universes u v w w'
+universe u v w w'
 
 inductive color
 | Red | Black

tests/bench/rbmap_checkpoint.lean

@@ -9,7 +9,7 @@ import Init.Data.List.BasicAux
 import Init.Data.String
 import Init.System.IO
 
-universes u v w w'
+universe u v w w'
 
 inductive color
 | Red | Black

tests/bench/rbmap_checkpoint2.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import init.coe init.data.option.basic init.system.io
 
-universes u v w w'
+universe u v w w'
 
 inductive color
 | Red | Black

tests/compiler/lazylist.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 
-universes u v w
+universe u v w
 
 inductive LazyList (α : Type u)
 | nil                               : LazyList α

tests/lean/223.lean

@@ -1,4 +1,4 @@
-universes u v
+universe u v
 
 inductive Imf {α : Type u} {β : Type v} (f : α → β) : β → Type (max u v)
 | mk : (a : α) → Imf f (f a)

tests/lean/276.lean

@@ -1,4 +1,4 @@
-universes u v
+universe u v
 
 -- `Type u` version can be defined without this option, but I get the same error
 set_option bootstrap.inductiveCheckResultingUniverse false in

tests/lean/343.lean

@@ -14,7 +14,7 @@ def Catish : CatIsh :=
     Hom := FunctorIsh
   }
 
-universes m o
+universe m o
 unif_hint (mvar : CatIsh) where
   Catish.{m,o} =?= mvar |- mvar.Obj =?= CatIsh.{m,o}
 

tests/lean/PPRoundtrip.lean

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

tests/lean/autoBoundImplicits2.lean

@@ -30,7 +30,7 @@ set_option autoBoundImplicitLocal false in
 def g2 {α : Type u /- Error -/} (a : α) : α :=
   a
 
-def g3 {α : Type β /- Error greek letters are not valid auto names for universes -/} (a : α) : α :=
+def g3 {α : Type β /- Error greek letters are not valid auto names for universe -/} (a : α) : α :=
   a
 
 def g4 {α : Type v} (a : α) : α :=

tests/lean/bigUnivOffsets.lean

@@ -1,5 +1,5 @@
 #check Type 100000000
 
-universes u
+universe u
 
 #check Type (u + 10000000)

tests/lean/binderCacheIssue.lean

@@ -1,4 +1,4 @@
-universes u v w
+universe u v w
 
 class Funtype (N : Sort u) (O : outParam (Sort v)) (T : outParam (Sort w)) :=
   pack : O -> N

tests/lean/doSeqRightIssue.lean

@@ -1,6 +1,6 @@
 --
 set_option autoBoundImplicitLocal false
-universes u
+universe u
 variable {α : Type u}
 variable {β : α → Type v}
 

tests/lean/inductionErrors.lean

@@ -1,4 +1,4 @@
-universes u
+universe u
 
 axiom elimEx (motive : Nat → Nat → Sort u) (x y : Nat)
   (diag  : (a : Nat) → motive a a)

tests/lean/inductive1.lean

@@ -14,7 +14,7 @@ inductive T2 : Type -- Error resulting universe mismatch
 end
 
 -- Test3
-universes u v
+universe u v
 mutual
 
 inductive T1 (x : Nat) : Type u

tests/lean/match1.lean

@@ -65,7 +65,7 @@ fun { x := x, ..} => { y := x }
 theorem ex2 : f1 { x := 10 } = { y := 10 } :=
 rfl
 
-universes u
+universe u
 
 inductive Vec (α : Type u) : Nat → Type u
 | nil : Vec α 0

tests/lean/match3.lean

@@ -8,7 +8,7 @@ match x with
 #eval f 0
 #eval f 30
 
-universes u
+universe u
 
 theorem ex1 {α : Sort u} {a b : α} (h : a ≅ b) : a = b :=
 match α, a, b, h with
@@ -57,7 +57,7 @@ theorem ex8 {a1 a2 : {x // p x}} (h : a1.val = a2.val) : a1 = a2 :=
 match a1, a2, h with
 | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
-universes v
+universe v
 variable {β : α → Type v}
 
 theorem ex9 {p₁ p₂ : Sigma (fun a => β a)} (h₁ : p₁.1 = p₂.1) (h : p₁.2 ≅ p₂.2) : p₁ = p₂ :=

tests/lean/pplevel.lean

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

tests/lean/run/CoeNew.lean

@@ -1,6 +1,6 @@
 
 
-universes u v w
+universe u v w
 
 instance boolToNat : Coe Bool Nat :=
 { coe := fun b => cond b 1 0 }

tests/lean/run/casesUsing.lean

@@ -4,7 +4,7 @@ open Lean
 open Lean.Meta
 open Lean.Elab.Tactic
 
-universes u
+universe u
 axiom elimEx (motive : Nat → Nat → Sort u) (x y : Nat)
   (diag  : (a : Nat) → motive a a)
   (upper : (delta a : Nat) → motive a (a + delta.succ))

tests/lean/run/catchThe.lean

@@ -3,7 +3,7 @@ import Lean.Meta
 open Lean
 open Lean.Meta
 
-universes u v w
+universe u v w
 
 abbrev M := ExceptT String MetaM
 

tests/lean/run/closure1.lean

@@ -3,7 +3,7 @@ import Lean
 open Lean
 open Lean.Meta
 
-universes u
+universe u
 
 inductive Vec (α : Type u) : Nat → Type u
 | nil      : Vec α 0

tests/lean/run/coeSort1.lean

@@ -1,6 +1,6 @@
 --
 
-universes u
+universe u
 
 def Below (n : Nat) : Nat → Prop :=
   (· < n)

tests/lean/run/concatElim.lean

@@ -1,4 +1,4 @@
-universes u
+universe u
 
 def concat {α} : List α → α → List α
   | [],    a => [a]

tests/lean/run/def2.lean

@@ -5,7 +5,7 @@ inductive Vec.{u} (α : Type u) : Nat → Type u
 | cons : α → {n : Nat} → Vec α n → Vec α (n+1)
 
 open Vec
-universes u
+universe u
 
 variable {α : Type u}
 variable (f : α → α → α)

tests/lean/run/def7.lean

@@ -9,7 +9,7 @@ def szn.{u} {α : Type u} (n : Nat) : InfTree α → InfTree α → Nat
 | node c, leaf b => 0
 | node c, node d => szn n (c n) (d n)
 
-universes u
+universe u
 
 theorem ex1 {α : Type u} (n : Nat) (c : Nat → InfTree α) (d : Nat → InfTree α) : szn n (node c) (node d) = szn n (c n) (d n) :=
 rfl

tests/lean/run/def8.lean

@@ -7,7 +7,7 @@ def g : List Nat → List Nat → Nat
 | x::xs,      y::ys => g xs ys + y
 | x::xs,      []    => g xs []
 
-universes u v
+universe u v
 
 inductive Imf {α : Type u} {β : Type v} (f : α → β) : β → Type (max u v)
 | mk : (a : α) → Imf f (f a)

tests/lean/run/depElim1.lean

@@ -6,7 +6,7 @@ open Lean.Meta.Match
 
 /- Infrastructure for testing -/
 
-universes u v
+universe u v
 
 def check (x : Bool) : IO Unit := do
 unless x do

tests/lean/run/forBodyResultTypeIssue.lean

@@ -14,7 +14,7 @@ rfl
 theorem ex2 : (f [1, 0, 3] |>.run' 0) = Except.error "contains zero" :=
 rfl
 
-universes u
+universe u
 
 abbrev N := ExceptT (ULift.{u} String) Id
 

tests/lean/run/forInUniv.lean

@@ -1,5 +1,5 @@
 
-universes u
+universe u
 
 def f {α : Type u} [BEq α] (xs : List α) (y : α) : α := do
 for x in xs do

tests/lean/run/inductive1.lean

@@ -11,7 +11,7 @@ inductive L2.{u} (α : Type u)
 
 #check @L2.cons
 
-universes u v
+universe u v
 variable (α : Type u)
 
 inductive A (β : Type v)

tests/lean/run/inj2.lean

@@ -1,4 +1,4 @@
-universes u v
+universe u v
 
 inductive Vec2 (α : Type u) (β : Type v) : Nat → Type (max u v)
 | nil  : Vec2 α β 0

tests/lean/run/injective.lean

@@ -1,4 +1,4 @@
-universes u v
+universe u v
 
 structure InjectiveFunction (α : Type u) (β : Type v) where
   fn  : α → β

tests/lean/run/instanceWhere.lean

@@ -1,5 +1,5 @@
 namespace Exp
-universes u v w
+universe u v w
 
 def StateT' (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
   σ → m (α × σ)

tests/lean/run/matchArrayLit.lean

@@ -1,4 +1,4 @@
-universes u v
+universe u v
 
 theorem eqLitOfSize0 {α : Type u} (a : Array α) (hsz : a.size = 0) : a = #[] :=
 a.toArrayLitEq 0 hsz

tests/lean/run/matcherElimUniv.lean

@@ -1,5 +1,5 @@
 
-universes u
+universe u
 
 def len {α : Type u} : List α → List α → Nat
 | [],    bs => bs.length

tests/lean/run/meta2.lean

@@ -623,7 +623,7 @@ do
 
 #eval tst40
 
-universes u
+universe u
 structure A (α : Type u) :=
 (x y : α)
 

tests/lean/run/new_compiler.lean

@@ -1,6 +1,6 @@
 
 
-universes u v w r s
+universe u v w r s
 
 set_option trace.compiler.stage1 true
 -- set_option pp.explicit true

tests/lean/run/new_inductive.lean

@@ -1,4 +1,4 @@
-universes u v
+universe u v
 
 inductive myList (α : Type u)
 | nil  : myList α

tests/lean/run/new_inductive2.lean

@@ -1,6 +1,6 @@
 
 
-universes u v
+universe u v
 
 inductive arrow (α : Type u) (β : Type v)
 | mk : (α → β) → arrow α β

tests/lean/run/newfrontend1.lean

@@ -305,7 +305,7 @@ def altTst3 {m σ} [Alternative m] [Monad m] : Alternative (StateT σ m) :=
 #check_failure 1 + true
 
 /-
-universes u v
+universe u v
 
 /-
   MonadFunctorT.{u ?M_1 v} (λ (β : Type u), m α) (λ (β : Type u), m' α) n n'

tests/lean/run/proofIrrelFVar.lean

@@ -1,5 +1,5 @@
 
-universes u
+universe u
 variable {α : Type u} {p : α → Prop}
 
 theorem ex (a : α) (h1 h2 : p a) (h : Subtype.mk a h1 = Subtype.mk a h1) : Subtype.mk a h1 = Subtype.mk a h2 :=

tests/lean/run/rc_tests.lean

@@ -1,5 +1,5 @@
 
-universes u v
+universe u v
 
 -- set_option pp.binder_types false
 set_option pp.explicit true

tests/lean/run/struct2.lean

@@ -1,4 +1,4 @@
-universes u v w
+universe u v w
 
 structure A (α : Type u) :=
 (f : (β : Type u) → α → β → α)

tests/lean/run/struct3.lean

@@ -1,4 +1,4 @@
-universes u v
+universe u v
 
 class Bind2 (m : Type u → Type v) where
   bind : ∀ {α β : Type u}, m α → (α → m β) → m β

tests/lean/run/structInst2.lean

@@ -1,7 +1,7 @@
 import Init.Control.Option
 
 
-universes u v
+universe u v
 
 def OptionT2 (m : Type u → Type v) (α : Type u) : Type v :=
 m (Option α)

tests/lean/run/structInst3.lean

@@ -1,5 +1,5 @@
 
-universes u
+universe u
 
 namespace Ex1
 

tests/lean/run/structInst4.lean

@@ -1,4 +1,4 @@
-universes u
+universe u
 
 def a : Array ((Nat × Nat) × Bool) := #[]
 def b : Array Nat := #[]

tests/lean/run/subst.lean

@@ -1,4 +1,4 @@
-universes u
+universe u
 
 def f1 (n m : Nat) (x : Fin n) (h : n = m) : Fin m :=
 h ▸ x

tests/lean/run/unifhint3.lean

@@ -1,6 +1,6 @@
 /- Coercion pullback example from the paper "Hints in Unification" -/
 
-universes u
+universe u
 
 structure Monoid where
   α    : Type u

tests/lean/run/univIssue.lean

@@ -1,4 +1,4 @@
-universes u v
+universe u v
 
 @[inline] def ex1 {σ : Type u} {m : Type u → Type v} [Functor m] {α : Type u} (x : StateT σ m α) (s : σ) : m α :=
   Functor.map Prod.fst (x s)

tests/lean/univInference.lean

@@ -1,5 +1,5 @@
 
-universes w₁ w₂ w₃
+universe w₁ w₂ w₃
 
 namespace Struct
 structure S1.{r, s} (α : Type s) : Type (max s r) :=

tests/lean/unused_univ.lean

@@ -5,7 +5,7 @@ variable (y : Nat)
 def f.{u} (x : Nat) : Nat := -- error unused universe parameter 'u'
 x
 
-universes u
+universe u
 
 def f.{v, w} (α : Type v) (a : α) : α := -- error unused universe parameter 'w'
 a