doc: replace variables

doc/implicit.md

@@ -75,8 +75,8 @@ section
   def ident := x
 end
 
-variables (α β : Type u)
-variables (a : α) (b : β)
+variable (α β : Type u)
+variable (a : α) (b : β)
 
 #check ident
 #check ident a
@@ -115,7 +115,7 @@ the arguments made explicit.
 
 ```lean
 # def ident {α : Type u} (a : α) : α := a
-variables (α β : Type)
+variable (α β : Type)
 
 #check @ident           -- {α : Type u} → α → α
 #check @ident α         -- α → α

doc/lean3changes.md

@@ -48,7 +48,7 @@ for consuming implicit arguments. We are still exploring this feature and analyz
 here is the example in the link above using Lean 4 implicit lambdas.
 
 ```lean
-# variables (ρ : Type) (m : Type → Type) [Monad m]
+# variable (ρ : Type) (m : Type → Type) [Monad m]
 instance : Monad (ReaderT ρ m) where
   pure := ReaderT.pure
   bind := ReaderT.bind
@@ -159,7 +159,7 @@ def g {α} [Add α] (a : α) (b? : Option α := none) (c : α) : α :=
   | none   => a + c
   | some b => a + b + c
 
-variables {α} [Add α]
+variable {α} [Add α]
 
 example : g = fun (a c : α) => a + c := rfl
 

doc/sections.md

@@ -12,10 +12,10 @@ def doThrice (α : Type) (h : α → α) (x : α) : α :=
   h (h (h x))
 ```
 
-Lean provides us with the ``variable`` and ``variables`` commands to make such declarations look more compact:
+Lean provides us with the ``variable`` command to make such declarations look more compact:
 
 ```lean
-variables (α β γ : Type)
+variable (α β γ : Type)
 
 def compose (g : β → γ) (f : α → β) (x : α) : γ :=
   g (f x)
@@ -28,8 +28,8 @@ def doThrice (h : α → α) (x : α) : α :=
 ```
 We can declare variables of any type, not just ``Type`` itself:
 ```lean
-variables (α β γ : Type)
-variables (g : β → γ) (f : α → β) (h : α → α)
+variable (α β γ : Type)
+variable (g : β → γ) (f : α → β) (h : α → α)
 variable (x : α)
 
 def compose := g (f x)
@@ -42,7 +42,7 @@ def doThrice := h (h (h x))
 ```
 Printing them out shows that all three groups of definitions have exactly the same effect.
 
-The ``variable`` and ``variables`` commands instruct Lean to insert the declared variables as bound variables in definitions that refer to them.
+The ``variable`` command instruct Lean to insert the declared variables as bound variables in definitions that refer to them.
 Lean is smart enough to figure out which variables are used explicitly or implicitly in a definition. We can therefore proceed as
 though ``α``, ``β``, ``γ``, ``g``, ``f``, ``h``, and ``x`` are fixed objects when we write our definitions, and let Lean abstract
 the definitions for us automatically.
@@ -52,8 +52,8 @@ Sometimes, however, it is useful to limit the scope of a variable. For that purp
 
 ```lean
 section useful
-  variables (α β γ : Type)
-  variables (g : β → γ) (f : α → β) (h : α → α)
+  variable (α β γ : Type)
+  variable (g : β → γ) (f : α → β) (h : α → α)
   variable (x : α)
 
   def compose := g (f x)