feat: subsume variables under variable

/cc @leodemoura

src/Lean/Elab/Command.lean

@@ -525,21 +525,13 @@ def elabOpenRenaming (n : SyntaxNode) : CommandElabM Unit := do
   else
     elabOpenRenaming body
 
-@[builtinCommandElab «variable»] def elabVariable : CommandElab := fun n => do
-  -- `variable` bracketedBinder
-  let binder := n[1]
-  -- Try to elaborate `binder` for sanity checking
-  runTermElabM none fun _ => Term.withAutoBoundImplicitLocal <|
-    Term.elabBinder binder (catchAutoBoundImplicit := true) fun _ => pure ()
-  modifyScope fun scope => { scope with varDecls := scope.varDecls.push binder }
-
-@[builtinCommandElab «variables»] def elabVariables : CommandElab := fun n => do
-  -- `variables` bracketedBinder+
-  let binders := n[1].getArgs
-  -- Try to elaborate `binders` for sanity checking
-  runTermElabM none fun _ => Term.withAutoBoundImplicitLocal <|
-    Term.elabBinders binders (catchAutoBoundImplicit := true) fun _ => pure ()
-  modifyScope fun scope => { scope with varDecls := scope.varDecls ++ binders }
+@[builtinCommandElab «variable»] def elabVariable : CommandElab
+  | `(variable $binders*) => do
+    -- Try to elaborate `binders` for sanity checking
+    runTermElabM none fun _ => Term.withAutoBoundImplicitLocal <|
+      Term.elabBinders binders (catchAutoBoundImplicit := true) fun _ => pure ()
+    modifyScope fun scope => { scope with varDecls := scope.varDecls ++ binders }
+  | _ => throwUnsupportedSyntax
 
 open Meta
 

src/Lean/Parser/Command.lean

@@ -66,8 +66,7 @@ declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant»
 @[builtinCommandParser] def «section»      := parser! "section " >> optional ident
 @[builtinCommandParser] def «namespace»    := parser! "namespace " >> ident
 @[builtinCommandParser] def «end»          := parser! "end " >> optional ident
-@[builtinCommandParser] def «variable»     := parser! "variable" >> Term.bracketedBinder
-@[builtinCommandParser] def «variables»    := parser! "variables" >> many1 Term.bracketedBinder
+@[builtinCommandParser] def «variable»     := parser! "variable" >> many1 Term.bracketedBinder
 @[builtinCommandParser] def «universe»     := parser! "universe " >> ident
 @[builtinCommandParser] def «universes»    := parser! "universes " >> many1 ident
 @[builtinCommandParser] def check          := parser! "#check " >> termParser

tests/bench/rbmap.lean

@@ -19,7 +19,7 @@ inductive Tree
 | Leaf  {}                                                                       : Tree
 | Node  (color : color) (lchild : Tree) (key : Nat) (val : Bool) (rchild : Tree) : Tree
 
-variables {σ : Type w}
+variable {σ : Type w}
 open color Nat Tree
 
 def fold (f : Nat → Bool → σ → σ) : Tree → σ → σ

tests/bench/rbmap2.lean

@@ -15,7 +15,7 @@ inductive Tree
 | Leaf  {}                                                                       : Tree
 | Node  (color : color) (lchild : Tree) (key : Nat) (val : Bool) (rchild : Tree) : Tree
 
-variables {σ : Type w}
+variable {σ : Type w}
 open color Nat Tree
 
 def fold (f : Nat → Bool → σ → σ) : Tree → σ → σ

tests/bench/rbmap3.lean

@@ -16,7 +16,7 @@ instance Rbcolor.DecidableEq : DecidableEq Rbcolor :=
   (Rbcolor.casesOn b (isFalse (fun h => Rbcolor.noConfusion h)) (isTrue rfl))}
 
 namespace Rbnode
-variables {α : Type u} {β : α → Type v} {σ : Type w}
+variable {α : Type u} {β : α → Type v} {σ : Type w}
 
 open Rbcolor
 
@@ -114,7 +114,7 @@ def setBlack : Rbnode α β → Rbnode α β
 | n                  => n
 
 section insert
-variables (lt : α → α → Prop) [DecidableRel lt]
+variable (lt : α → α → Prop) [DecidableRel lt]
 
 def ins (x : α) (vx : β x) : Rbnode α β → Rbnode α β
 | leaf             => Node red leaf x vx leaf
@@ -176,7 +176,7 @@ def Rbmap (α : Type u) (β : Type v) (lt : α → α → Prop) : Type (max u v)
 ⟨leaf, WellFormed.leafWff lt⟩
 
 namespace Rbmap
-variables {α : Type u} {β : Type v} {σ : Type w} {lt : α → α → Prop}
+variable {α : Type u} {β : Type v} {σ : Type w} {lt : α → α → Prop}
 
 def depth (f : Nat → Nat → Nat) (t : Rbmap α β lt) : Nat :=
 t.val.depth f
@@ -209,7 +209,7 @@ t.val.depth f
 instance [Repr α] [Repr β] : Repr (Rbmap α β lt) :=
 ⟨fun t => "rbmapOf " ++ repr t.toList⟩
 
-variables [DecidableRel lt]
+variable [DecidableRel lt]
 
 def insert : Rbmap α β lt → α → β → Rbmap α β lt
 | ⟨t, w⟩,   k, v => ⟨t.insert lt k v, WellFormed.insertWff w rfl⟩

tests/bench/rbmap4.lean

@@ -15,7 +15,7 @@ inductive Tree
 | Leaf  {}                                                                       : Tree
 | Node  (color : color) (lchild : Tree) (key : Nat) (val : Bool) (rchild : Tree) : Tree
 
-variables {σ : Type w}
+variable {σ : Type w}
 open color Nat Tree
 
 def fold (f : Nat → Bool → σ → σ) : Tree → σ → σ

tests/bench/rbmap500k.lean

@@ -15,7 +15,7 @@ inductive Tree
 | Leaf  {}                                                                       : Tree
 | Node  (color : color) (lchild : Tree) (key : Nat) (val : Bool) (rchild : Tree) : Tree
 
-variables {σ : Type w}
+variable {σ : Type w}
 open color Nat Tree
 
 def fold (f : Nat → Bool → σ → σ) : Tree → σ → σ

tests/bench/rbmap_checkpoint.lean

@@ -21,7 +21,7 @@ inductive Tree
 
 instance : Inhabited Tree := ⟨Tree.Leaf⟩
 
-variables {σ : Type w}
+variable {σ : Type w}
 open color Nat Tree
 
 def fold (f : Nat → Bool → σ → σ) : Tree → σ → σ

tests/bench/rbmap_checkpoint2.lean

@@ -17,7 +17,7 @@ inductive Tree
 
 instance : Inhabited Tree := ⟨Tree.Leaf⟩
 
-variables {σ : Type w}
+variable {σ : Type w}
 open color Nat Tree
 
 def fold (f : Nat → Bool → σ → σ) : Tree → σ → σ

tests/bench/unionfind.lean

@@ -1,7 +1,7 @@
 #lang lean4
 def StateT' (m : Type → Type) (σ : Type) (α : Type) := σ → m (α × σ)
 namespace StateT'
-variables {m : Type → Type} [Monad m] {σ : Type} {α β : Type}
+variable {m : Type → Type} [Monad m] {σ : Type} {α β : Type}
 @[inline] protected def pure (a : α) : StateT' m σ α := fun s => pure (a, s)
 @[inline] protected def bind (x : StateT' m σ α) (f : α → StateT' m σ β) : StateT' m σ β := fun s => do let (a, s') ← x s; f a s'
 @[inline] def read : StateT' m σ σ := fun s => pure (s, s)
@@ -13,7 +13,7 @@ end StateT'
 
 def ExceptT' (m : Type → Type) (ε : Type) (α : Type) := m (Except ε α)
 namespace ExceptT'
-variables {m : Type → Type} [Monad m] {ε : Type} {α β : Type}
+variable {m : Type → Type} [Monad m] {ε : Type} {α β : Type}
 @[inline] protected def pure (a : α) : ExceptT' m ε α := (pure (Except.ok a) : m (Except ε α))
 @[inline] protected def bind (x : ExceptT' m ε α) (f : α → ExceptT' m ε β) : ExceptT' m ε β :=
 (do { let v ← x; match v with

tests/compiler/lazylist.lean

@@ -17,7 +17,7 @@ def List.toLazy {α : Type u} : List α → LazyList α
 | h::t   => LazyList.cons h (toLazy t)
 
 namespace LazyList
-variables {α : Type u} {β : Type v} {δ : Type w}
+variable {α : Type u} {β : Type v} {δ : Type w}
 
 instance : Inhabited (LazyList α) :=
 ⟨nil⟩

tests/elabissues/variable_universe_bug.lean

@@ -11,6 +11,6 @@ universes v u
 class Category (C : Type u) :=
 (Hom : ∀ (X Y : C), Type v)
 
-variables {C : Type u} [Category.{v, u} C]
+variable {C : Type u} [Category.{v, u} C]
 
 def End (X : C) := Category.Hom X X -- invalid reference to undefined universe level parameter 'v'

tests/elabissues/vars.lean

@@ -2,7 +2,7 @@ def f1 {α} [ToString α] (a : α) : String := -- works
 ">> " ++ toString a
 
 -- Moving `{α} [ToString α]` to a `variables` break the example
-variables {α} [ToString α]
+variable {α} [ToString α]
 def f2 (a : α) : String :=
 ">> " ++ toString a
 
@@ -11,7 +11,7 @@ class Dummy (α : Type) := (val : α)
 /- The following fails because `variables {α : Type _} [Dummy α]` is processed as `variable {α : Type _} variable [Dummy α]`
    The first command elaborates `α` as `variable {α : Type u_1}` where `u_1` is a fresh metavariable.
    That is, in Lean3, metavariables are resolved before the end of the command. -/
-variables {α : Type _} [Dummy α]
+variable {α : Type _} [Dummy α]
 
 def f3 {α : Type _} [Dummy α] : α := -- works
 Dummy.val α

tests/lean/autoBoundImplicits1.lean

@@ -26,7 +26,7 @@ def Vec.map3 (xs : Vec α n) (f : α → β) : Vec β n := -- Errors, unknown id
 
 def double [Add α] (a : α) := a + a
 
-variables (xs : Vec α n) -- works
+variable (xs : Vec α n) -- works
 
 def f := xs
 

tests/lean/auxDeclIssue.lean

@@ -5,7 +5,7 @@ by {
    assumption -- should not use the auxiliary declaration `ex1 : False`
 }
 
-variables (x y : Nat) in
+variable (x y : Nat) in
 theorem ex2 : x = y :=
 by {
   subst x; -- should not use the auxiliary declaration `ex2 : x = y`

tests/lean/collectDepsIssue.lean

@@ -1,6 +1,6 @@
 
 
-variables {α : Type} in
+variable {α : Type} in
 def f (a : α) : List α :=
 _
 

tests/lean/doSeqRightIssue.lean

@@ -1,8 +1,8 @@
 --
 set_option autoBoundImplicitLocal false
 universes u
-variables {α : Type u}
-variables {β : α → Type v}
+variable {α : Type u}
+variable {β : α → Type v}
 
 theorem ex {p₁ p₂ : Sigma (fun a => β a)} (h₁ : p₁.1 = p₂.1) (h : p₁.2 ≅ p₂.2) : p₁ = p₂ :=
 match p₁, p₂, h₁, h with

tests/lean/doSeqRightIssue.lean.expected.out

@@ -1 +1 @@
-doSeqRightIssue.lean:5:24-5:25: error: unknown universe level 'v'
+doSeqRightIssue.lean:5:23-5:24: error: unknown universe level 'v'

tests/lean/match3.lean

@@ -48,14 +48,14 @@ match he:xs with
 | []   => False.elim $ h he
 | x::_ => x
 
-variables {α : Type u} {p : α → Prop}
+variable {α : Type u} {p : α → Prop}
 
 theorem ex8 {a1 a2 : {x // p x}} (h : a1.val = a2.val) : a1 = a2 :=
 match a1, a2, h with
 | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
 universes v
-variables {β : α → Type v}
+variable {β : α → Type v}
 
 theorem ex9 {p₁ p₂ : Sigma (fun a => β a)} (h₁ : p₁.1 = p₂.1) (h : p₁.2 ≅ p₂.2) : p₁ = p₂ :=
 match p₁, p₂, h₁, h with

tests/lean/precissues.lean

@@ -23,7 +23,7 @@ def f (x : Nat) (g : Nat → Nat) := g x
 #check 0 = have Nat from 1; this
 #check 0 = let x := 0; x
 
-variables (p q r : Prop)
+variable (p q r : Prop)
 macro_rules | `(¬ $p) => `(Not $p)
 
 #check p ↔ ¬ q

tests/lean/protected.lean

@@ -55,7 +55,7 @@ def S (σ : Type) (m : Type → Type) (α : Type) :=
 σ → m (α × σ)
 
 namespace S
-variables {σ : Type} {m : Type → Type} [Monad m] {α : Type}
+variable {σ : Type} {m : Type → Type} [Monad m] {α : Type}
 
 protected def pure (a : α) : S σ m α :=
 fun s => pure (a, s) -- This `pure` is the top-level one. The `pure` being defined here is called `S.pure`.

tests/lean/run/492_lean3.lean

@@ -4,7 +4,7 @@ def foo.f' {α : Type} [c : foo α] : α := foo.f
 #print foo.f  -- def foo.f : {α : Type} → [self : foo α] → α
 #print foo.f' -- def foo.f' : {α : Type} → [c : foo α] → α
 
-variables {α : Type} [c : foo α]
+variable {α : Type} [c : foo α]
 #check c.f  -- ok
 #check c.f' -- ok
 
@@ -14,7 +14,7 @@ def bar.f' : bar → ∀ {m : Nat}, m = 0 := bar.f
 #print bar.f  -- def bar.f  : bar → ∀ {m : ℕ}, m = 0
 #print bar.f' -- def bar.f' : bar → ∀ {m : ℕ}, m = 0
 
-variables (h : bar) (m : Nat)
+variable (h : bar) (m : Nat)
 
 #check (h.f : ∀ {m : Nat}, m = 0) -- ok
 #check (h.f : m = 0)  -- ok

tests/lean/run/Daniel1.lean

@@ -7,7 +7,7 @@ def small (ps : Array (Nat × Nat)) : Array (Nat × Nat) :=
 
 #eval small #[(1, 2), (0, 3), (2, 4)]
 
-variables {α β : Type} [Inhabited α] [Inhabited β]
+variable {α β : Type} [Inhabited α] [Inhabited β]
 
 def P (xys : Array (α × β)) (f : α → β) : Prop := True
 

tests/lean/run/Dorais1.lean

@@ -8,7 +8,7 @@ inductive Path {α : Type _} : Tree α → Type _
 | right (tl tr : Tree α) : Path tr → Path (Tree.branch  tl tr)
 
 section map
-variables {α : Type _} {β : Type _} (f : α → β)
+variable {α : Type _} {β : Type _} (f : α → β)
 
 protected def Tree.map : Tree α → Tree β
 | Tree.leaf x => Tree.leaf (f x)

tests/lean/run/KyleAlg.lean

@@ -112,21 +112,21 @@ class IntegralDomain (α : Type u) extends CommRing α, Domain α
 attribute [instance] IntegralDomain.mk
 
 section test1
-variables (α : Type u) [h : CommMonoid α]
+variable (α : Type u) [h : CommMonoid α]
 example : Semigroup α := inferInstance
 example : Monoid α := inferInstance
 example : CommSemigroup α := inferInstance
 end test1
 
 section test2
-variables (β : Type u) [CommSemigroup β] [One β] [OneUnit β]
+variable (β : Type u) [CommSemigroup β] [One β] [OneUnit β]
 example : Monoid β := inferInstance
 example : CommMonoid β := inferInstance
 example : Semigroup β := inferInstance
 end test2
 
 section test3
-variables (β : Type u) [Mul β] [One β] [MulAssoc β] [OneUnit β]
+variable (β : Type u) [Mul β] [One β] [MulAssoc β] [OneUnit β]
 example : Monoid β := inferInstance
 example : Semigroup β := inferInstance
 end test3

tests/lean/run/coeIssue1.lean

@@ -38,5 +38,5 @@ def sext {s:Nat} (x : Expr (bv s)) (n:Nat) : Expr (bv (s+n)) := Expr.sextC x (s+
 
 open MCType
 
-variables {u:Nat} (e : Expr (bv 64))
+variable {u:Nat} (e : Expr (bv 64))
 #check (bvmul (sext (Reg.rax 64) 64) (sext e 64) : Expr (bv 128))

tests/lean/run/concatElim.lean

@@ -14,7 +14,7 @@ def dropLast {α} : List α → List α
   | [a]   => []
   | a::as => a :: dropLast as
 
-variables {α}
+variable {α}
 
 theorem concatEq (xs : List α) (h : xs ≠ []) : concat (dropLast xs) (last xs h) = xs := by
   match xs, h with

tests/lean/run/def13.lean

@@ -1,4 +1,4 @@
-variables {α} (p : α → Prop) [DecidablePred p]
+variable {α} (p : α → Prop) [DecidablePred p]
 
 def filter : List α → List α
 | []    => []

tests/lean/run/def2.lean

@@ -7,8 +7,8 @@ inductive Vec.{u} (α : Type u) : Nat → Type u
 open Vec
 universes u
 
-variables {α : Type u}
-variables (f : α → α → α)
+variable {α : Type u}
+variable (f : α → α → α)
 
 def mapHead1 : {n : Nat} → Vec α n → Vec α n → Vec α n
 | _, nil, nil => nil

tests/lean/run/frontend1.lean

@@ -1,225 +0,0 @@
-#lang lean4
-import Lean.Elab
-open Lean
-open Lean.Elab
-
-def runM (input : String) (failIff : Bool := true) : CoreM Unit := do
-let env  ← getEnv;
-let opts ← getOptions;
-let (env, messages) ← process input env opts;
-messages.forM fun msg => do IO.println (← msg.toString)
-when (failIff && messages.hasErrors) $ throwError "errors have been found";
-when (!failIff && !messages.hasErrors) $ throwError "there are no errors";
-pure ()
-
-def fail (input : String) : CoreM Unit :=
-runM input false
-
-def M := IO Unit
-
-def zero := 0
-def one := 1
-def two := 2
-def hello : String := "hello"
-
-def act1 : IO String :=
-pure "hello"
-
-#eval runM "#check @Add.add"
-#eval runM "#check [zero, one, two]"
-#eval runM "#check id $ Nat.succ one"
-#eval runM "#check Add.add one two"
-#eval runM "#check one + two > one ∧ True"
-#eval runM "#check act1 >>= IO.println"
-#eval runM "#check one + two == one"
-#eval fail "#check one + one + hello == hello ++ one"
-#eval runM "#check Nat.add one $ Nat.add one two"
-
-#eval runM
-"universe u universe v
- export ToString (toString)
- section namespace foo.bla end bla end foo
- variable (p q : Prop)
- variable (_ b : _)
- variable {α : Type}
- variable {m : Type → Type}
- variable [Monad m]
- #check m
- #check Type
- #check Prop
- #check toString zero
- #check id Nat.zero (α := Nat)
- #check id _ (α := Nat)
- #check id Nat.zero
- #check id (α := Nat)
- #check @id Nat
- #check p
- #check α
- #check Nat.succ
- #check Nat.add
- #check id
- #check forall (α : Type), α → α
- #check (α : Type) → α → α
- #check {α : Type} → {β : Type} → M → (α → β) → α → β
- #check ()
- end"
-
-structure S1 :=
-(x y : Nat := 0)
-
-structure S2 extends S1 :=
-(z : Nat := 0)
-
-def fD {α} [ToString α] (a b : α) : String :=
-toString a ++ toString b
-
-structure S3 :=
-(w : Nat := 0)
-(f : forall {α : Type} [ToString α], α → α → String := @fD)
-
-structure S4 extends S2, S3 :=
-(s : Nat := 0)
-
-def s4 : S4 := {}
-
-structure S (α : Type) :=
-(field1 : S4 := {})
-(field2 : S4 × S4 := ({}, {}))
-(field3 : α)
-(field4 : List α × Nat := ([], 0))
-(vec : Array (α × α) := #[])
-(map : Std.HashMap String α := {})
-
-inductive D (α : Type)
-| mk (a : α) (s : S4) : D α
-
-def s : S Nat := { field3 := 0 }
-def d : D Nat := D.mk 10 {}
-def i : Nat := 10
-def k : String := "hello"
-
-universes u
-
-class Monoid (α : Type u) :=
-(one : α)
-(mul : α → α → α)
-
-def m : Monoid Nat :=
-{ one := 1, mul := Nat.mul }
-
-def f (x y z : Nat) : Nat :=
-x + y + z
-
-#eval runM "#check s4.x"
-#eval runM "#check s.field1.x"
-#eval runM "#check s.field2.fst"
-#eval runM "#check s.field2.fst.w"
-#eval runM "#check s.1.x"
-#eval runM "#check s.2.1.x"
-#eval runM "#check d.1"
-#eval runM "#check d.2.x"
-#eval runM "#check s4.f s4.x"
-#eval runM "#check m.mul m.one"
-#eval runM "#check s.field4.1.length.succ"
-#eval runM "#check s.field4.1.map Nat.succ"
-#eval runM "#check s.vec[i].1"
-#eval runM "#check \"hello\""
-#eval runM "#check 1"
-#eval runM "#check Nat.succ 1"
-#eval runM "#check fun _ a (x y : Int) => x + y + a"
-#eval runM "#check (one)"
-#eval runM "#check ()"
-#eval runM "#check (one, two, zero)"
-#eval runM "#check (one, two, zero)"
-#eval runM "#check (1 : Int)"
-#eval runM "#check ((1, 2) : Nat × Int)"
-#eval runM "#check (· + one)"
-#eval runM "#check (· + · : Nat → Nat → Nat)"
-#eval runM "#check (f one · zero)"
-#eval runM "#check (f · · zero)"
-#eval runM "#check fun (_ b : Nat) => b + 1"
-
-def foo {α β} (a : α) (b : β) (a' : α) : α :=
-a
-
-def bla {α β} (f : α → β) (a : α) : β :=
-f a
-
--- #check fun x => foo x x.w s4 -- fails in old elaborator
--- #check bla (fun x => x.w) s4 -- fails in the old elaborator
--- #check #[1, 2, 3].foldl (fun r a => r.push a) #[] -- fails in the old elaborator
-
-#eval runM "#check fun x => foo x x.w s4"
-#eval runM "#check bla (fun x => x.w) s4"
-#eval runM "#check #[1, 2, 3].foldl (fun r a => r.push a) #[]"
-#eval runM "#check #[1, 2, 3].foldl (fun r a => (r.push a).push a) #[]"
-#eval runM "#check #[1, 2, 3].foldl (fun r a => ((r.push a).push a).push a) #[]"
-#eval runM "#check #[].push one |>.push two |>.push zero |>.size.succ"
-#eval runM "#check #[1, 2].foldl (fun r a => r.push a |>.push a |>.push a) #[]"
-#eval runM "#check #[1, 2].foldl (init := #[]) $ fun r a => r.push a |>.push a"
-
-#eval runM "#check let x := one + zero; x + x"
--- set_option trace.Elab true
-#eval runM "#check (fun x => let v := x.w; v + v) s4"
-#eval runM "#check fun x => foo x (let v := x.w; v + one) s4"
-#eval runM "#check fun x => foo x (let v := x.w; let w := x.x; v + w + one) s4"
-#eval fail "#check id.{1,1}"
-#eval fail "#check @id.{0} Nat"
-#eval runM "#check @id.{1} Nat"
-#eval runM "universes u #check id.{u}"
-#eval fail "universes u #check id.{v}"
-#eval runM "universes u #check Type u"
-#eval runM "universes u #check Sort u"
-#eval runM "#check Type 1"
-#eval runM "#check Type 0"
-#eval runM "universes u v #check Sort (max u v)"
-#eval runM "universes u v #check Type (max u v)"
-#eval runM "#check 'a'"
-#eval fail "#check #['a', \"hello\"]"
-#eval runM "#check fun (a : Array Nat) => a.size"
-#eval runM "#check if 0 = 1 then 'a' else 'b'"
-#eval runM "#check fun (i : Nat) (a : Array Nat) => if h : i < a.size then a.get (Fin.mk i h) else i"
-#eval runM "#check { x : Nat // x > 0 }"
-#eval runM "#check { x // x > 0 }"
-#eval runM "#check fun (i : Nat) (a : Array Nat) => if h : i < a.size then a.get ⟨i, h⟩ else i"
-#eval runM "#check Prod.fst ⟨1, 2⟩"
-#eval runM "#check let x := ⟨1, 2⟩; Prod.fst x"
-#eval runM "#check show Nat from 1"
-#eval runM "#check show Int from 1"
-#eval runM "#check have Nat from one + zero; this + this"
-#eval runM "#check have x : Nat from one + zero; x + x"
-#eval runM "#check have Nat := one + zero; this + this"
-#eval runM "#check have x : Nat := one + zero; x + x"
-
-#eval runM "variables {α β} axiom x (n : Nat) : α → α #check x 1 0"
-#eval runM "#check ToString.toString 0"
-#eval runM "@[instance] axiom newInst : ToString Nat #check newInst #check ToString.toString 0"
-#eval runM "variables {β σ} universes w1 w2 /-- Testing axiom -/ unsafe axiom Nat.aux (γ : Type w1) (v : Nat) : β → (α : Type _) → v = zero /- Nat.zero -/ → Array α #check @Nat.aux"
-#eval runM "def x : Nat := Nat.zero #check x"
-#eval runM "def x := Nat.zero #check x"
-#eval runM "open Lean.Parser def x := parser! symbol \"foo\" #check x"
-#eval runM "open Lean.Parser def x := parser!:50 symbol \"foo\" #check x"
-#eval runM "open Lean.Parser def x := tparser! symbol \"foo\" #check x"
-#eval runM "def x : Nat := 1 #check x"
-
-
-def g (x : Nat := zero) (y : Nat := one) (z : Nat := two) : Nat :=
-x + y + z
-
-def three := 3
-
-#eval runM "#check g"
-#eval runM "#check g (x := three) (z := zero)"
-#eval runM "#check g (y := three)"
-#eval runM "#check g (z := three)"
-#eval runM "#check g three (z := zero)"
-
-#eval runM "#check (fun stx => if True then let e := stx; Pure.pure e else Pure.pure stx : Nat → Id Nat)"
-#eval runM "constant n : Nat #check n"
-
-#eval fail "#check Nat.succ 'a'"
-
-#eval runM "universes u v #check Type (max u v)"
-#eval runM "universes u v #check Type (imax u v)"
-
-#eval fail "namespace Boo def f (x : Nat) := x def s := 'a' #check (fun x => f x) s end Boo"

tests/lean/run/incmd.lean

@@ -6,7 +6,7 @@ fun x => x
 
 #check @f
 
-variables {α : Type} {β : Type} in
+variable {α : Type} {β : Type} in
 variable (h : α → α) in
 set_option pp.raw.maxDepth 1000 in
 def g : α → β → α :=

tests/lean/run/new_inductive.lean

@@ -8,7 +8,7 @@ inductive myPair (α : Type u) (β : Type v)
 | mk : α → β → myPair α β
 
 mutual
-variables (α : Type u) (m : α → Type v)
+variable (α : Type u) (m : α → Type v)
 inductive bla : Nat → Type (max u v)
 | mk₁ (n : Nat) : α → boo n → bla (n+1)
 | mk₂ (a : α)   : m a → String → bla 0
@@ -54,7 +54,7 @@ inductive Rbnode (α : Type u)
 #check @Rbnode.brecOn
 
 namespace Rbnode
-variables {α : Type u}
+variable {α : Type u}
 
 constant insert (lt : α → α → Prop) [DecidableRel lt] (t : Rbnode α) (x : α) : Rbnode α := Rbnode.leaf
 

tests/lean/run/newfrontend1.lean

@@ -2,7 +2,7 @@ def x := 1
 
 #check x
 
-variables {α : Type}
+variable {α : Type}
 
 def f (a : α) : α :=
 a

tests/lean/run/partialApp.lean

@@ -26,7 +26,7 @@ match b? with
 | none   => a + c
 | some b => a + b + c
 
-variables {α} [Add α]
+variable {α} [Add α]
 
 theorem ex7 : g = fun (a c : α) => a + c :=
 rfl

tests/lean/run/proofIrrelFVar.lean

@@ -1,6 +1,6 @@
 
 universes u
-variables {α : Type u} {p : α → Prop}
+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 :=
 h

tests/lean/run/propagateExpectedType.lean

@@ -1,4 +1,4 @@
-variables {α : Type _} (r : α → α → Prop) (π : α → α)
+variable {α : Type _} (r : α → α → Prop) (π : α → α)
 
 inductive rel : α → α → Prop
 | of {x y} : r x y → rel x y

tests/lean/run/quasi_pattern_unification_approx_issue.lean

@@ -1,6 +1,6 @@
 
 
-variables {δ σ : Type}
+variable {δ σ : Type}
 
 def foo0 : StateT δ (StateT σ Id) σ :=
 getThe σ

tests/lean/run/structInst2.lean

@@ -7,7 +7,7 @@ def OptionT2 (m : Type u → Type v) (α : Type u) : Type v :=
 m (Option α)
 
 namespace OptionT2
-variables {m : Type u → Type v} [Monad m] {α β : Type u}
+variable {m : Type u → Type v} [Monad m] {α β : Type u}
 
 @[inline] protected def bind (ma : OptionT2 m α) (f : α → OptionT2 m β) : OptionT2 m β :=
 (do {

tests/lean/run/stuckMVarBug.lean

@@ -13,7 +13,7 @@ attribute [instance] B.mk B.Mul B.HasMulComm
 example [A α] [HasMulComm α] : B α := inferInstance
 
 section
-variables [A α] [HasMulComm α]
+variable [A α] [HasMulComm α]
 
 example : B α := by exact inferInstance
 

tests/lean/run/suffices.lean

@@ -1,4 +1,4 @@
-variables {a b c : Prop}
+variable {a b c : Prop}
 
 theorem ex1 (Ha : a) (Hab : a → b) (Hbc : b → c) : c :=
   suffices b from Hbc this

tests/lean/safeShadowing.lean

@@ -3,7 +3,7 @@ def f (x x : Nat) :=
   | 0          => x + 1
   | Nat.succ _ => x + 2
 
-variables {α : Type}
+variable {α : Type}
 
 #check fun (a : α) => a
 

tests/lean/zipper.lean

@@ -3,7 +3,7 @@ structure ListZipper (α : Type) :=
 
 -- set_option trace.compiler.ir.rc true
 
-variables {α : Type}
+variable {α : Type}
 
 namespace ListZipper
 

tests/playground/environment_extension.lean

@@ -8,7 +8,7 @@ namespace Lean
 constant EnvironmentExtension (entryTy stateTy : Type) : Type := Unit
 
 namespace EnvironmentExtension
-variables {entryTy stateTy : Type}
+variable {entryTy stateTy : Type}
 /-- Register a new environment extension. The Result should usually be bound to
     a top-Level definition, after which it can be used to access and modify the
     extension State. -/
@@ -26,7 +26,7 @@ variables {entryTy stateTy : Type}
   (addEntry : Π (init : Bool), environment → stateTy → entryTy → stateTy) :
   IO (EnvironmentExtension entryTy stateTy) := default _
 
-variables {entryTy' stateTy' : Type}
+variable {entryTy' stateTy' : Type}
 
 /- Register a dependency between two environment extensions.
    That is, whenever an entry `e` is added to `fromExt`,
@@ -60,7 +60,7 @@ def scopedExtsRef.init : IO (IO.Ref (List Info)) := IO.mkRef []
 @[init scopedExtsRef.init] private constant scopedExtsRef : IO.Ref (List Info) := default _
 def scopedExts : IO (List Info) := scopedExtsRef.get
 
-variables {entryTy stateTy : Type}
+variable {entryTy stateTy : Type}
 
 def register (key : Option String) (emptyState : stateTy)
   (addEntry : Π (init : Bool), environment → stateTy → entryTy → stateTy)

tests/playground/lazylist.lean

@@ -16,7 +16,7 @@ def List.toLazy {α : Type u} : List α → LazyList α
 | (h::t) := LazyList.cons h (List.toLazy t)
 
 namespace LazyList
-variables {α : Type u} {β : Type v} {δ : Type w}
+variable {α : Type u} {β : Type v} {δ : Type w}
 
 instance : Inhabited (LazyList α) :=
 ⟨nil⟩

tests/playground/parser/parser.lean

@@ -659,7 +659,7 @@ instance recParserLift (α ρ : Type) [ParserFnLift ρ] : ParserFnLift (RecParse
 inferInstanceAs (ParserFnLift (EnvParserFn (α → ρ) ρ))
 
 namespace RecParserFn
-variables {α ρ : Type}
+variable {α ρ : Type}
 
 @[inline] def recurse (a : α) : RecParserFn α ρ :=
 λ p, p a

tests/playground/uf1.lean

@@ -1,6 +1,6 @@
 def StateT (m : Type → Type) (σ : Type) (α : Type) := (Unit × σ) → m (α × σ)
 namespace StateT
-variables {m : Type → Type} [Monad m] {σ : Type} {α β : Type}
+variable {m : Type → Type} [Monad m] {σ : Type} {α β : Type}
 @[inline] protected def pure (a : α) : StateT m σ α := λ ⟨_, s⟩, pure (a, s)
 @[inline] protected def bind (x : StateT m σ α) (f : α → StateT m σ β) : StateT m σ β := λ p, do (a, s') ← x p, f a ((), s')
 @[inline] def read : StateT m σ σ := λ ⟨_, s⟩, pure (s, s)
@@ -12,7 +12,7 @@ end StateT
 
 def ExceptT (m : Type → Type) (ε : Type) (α : Type) := { e : Except ε Unit // e = Except.ok () } → m (Except ε α)
 namespace ExceptT
-variables {m : Type → Type} [Monad m] {ε : Type} {α β : Type}
+variable {m : Type → Type} [Monad m] {ε : Type} {α β : Type}
 @[inline] protected def pure (a : α) : ExceptT m ε α :=
 λ e, match e with
      | ⟨Except.ok _, h⟩    := pure (Except.ok a)

tests/playground/uf1_new.lean

@@ -1,6 +1,6 @@
 def StateT (m : Type → Type) (σ : Type) (α : Type) := (Unit × σ) → m (α × σ)
 namespace StateT
-variables {m : Type → Type} [Monad m] {σ : Type} {α β : Type}
+variable {m : Type → Type} [Monad m] {σ : Type} {α β : Type}
 @[inline] protected def pure (a : α) : StateT m σ α := λ ⟨_, s⟩, pure (a, s)
 @[inline] protected def bind (x : StateT m σ α) (f : α → StateT m σ β) : StateT m σ β := λ p, do (a, s') ← x p, f a ((), s')
 @[inline] def read : StateT m σ σ := λ ⟨_, s⟩, pure (s, s)
@@ -12,7 +12,7 @@ end StateT
 
 def ExceptT (m : Type → Type) (ε : Type) (α : Type) := m (Except ε α)
 namespace ExceptT
-variables {m : Type → Type} [Monad m] {ε : Type} {α β : Type}
+variable {m : Type → Type} [Monad m] {ε : Type} {α β : Type}
 @[inline] protected def pure (a : α) : ExceptT m ε α := (pure (Except.ok a) : m (Except ε α))
 @[inline] protected def bind (x : ExceptT m ε α) (f : α → ExceptT m ε β) : ExceptT m ε β :=
 (do { v ← x, match v with