From 2a341c01e0c8cdacf04147de0e80fe39ce19ed14 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 22 Jan 2021 18:38:49 +0100
Subject: [PATCH] doc: replace `variables`

---
 doc/implicit.md     |  6 +++---
 doc/lean3changes.md |  4 ++--
 doc/sections.md     | 14 +++++++-------
 3 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/doc/implicit.md b/doc/implicit.md
index 65ef591c06..dcda6a3399 100644
--- a/doc/implicit.md
+++ b/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 α         -- α → α
diff --git a/doc/lean3changes.md b/doc/lean3changes.md
index 672dbc3eec..b5216ec81c 100644
--- a/doc/lean3changes.md
+++ b/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
 
diff --git a/doc/sections.md b/doc/sections.md
index c6eb3e8243..ca4b0c7885 100644
--- a/doc/sections.md
+++ b/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)