From 53750ddae62bb3f30288ac061b3bbb7755768caa Mon Sep 17 00:00:00 2001
From: Mohamed Al-Fahim <31521089+MohamedAlFahim@users.noreply.github.com>
Date: Wed, 20 Jan 2021 20:22:37 +0000
Subject: [PATCH] chore: fix typos

---
 doc/tour.md       | 2 +-
 doc/typeobjs.md   | 2 +-
 src/Init/Coe.lean | 4 ++--
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/doc/tour.md b/doc/tour.md
index 17b1b9e66b..26c0f36954 100644
--- a/doc/tour.md
+++ b/doc/tour.md
@@ -60,7 +60,7 @@ end BasicFunctions
 
 ```lean
 -- Lean has first-class functions.
--- `twice` takes two argumes `f` and `a` where
+-- `twice` takes two arguments `f` and `a` where
 -- `f` is a function from natural numbers to natural numbers, and
 -- `a` is a natural number.
 def twice (f : Nat → Nat) (a : Nat) :=
diff --git a/doc/typeobjs.md b/doc/typeobjs.md
index 6b8948f9dd..d612266930 100644
--- a/doc/typeobjs.md
+++ b/doc/typeobjs.md
@@ -114,7 +114,7 @@ constant α : Type _
 #check α
 ```
 
-Several Lean 3 users use the shorhand `Type*` for `Type _`. The `Type*` notation is not builtin in Lean 4, but you can be easily define it using a `macro`.
+Several Lean 3 users use the shorhand `Type*` for `Type _`. The `Type*` notation is not builtin in Lean 4, but you can easily define it using a `macro`.
 ```lean
 macro "Type*" : term => `(Type _)
 
diff --git a/src/Init/Coe.lean b/src/Init/Coe.lean
index a551c061bc..7fe66f6e94 100644
--- a/src/Init/Coe.lean
+++ b/src/Init/Coe.lean
@@ -15,7 +15,7 @@ class Coe (α : Sort u) (β : Sort v) where
 class CoeTC (α : Sort u) (β : Sort v) where
   coe : α → β
 
-/- Expensive coercion that can only appear at the beggining of a sequence of coercions. -/
+/- Expensive coercion that can only appear at the beginning of a sequence of coercions. -/
 class CoeHead (α : Sort u) (β : Sort v) where
   coe : α → β
 
@@ -115,7 +115,7 @@ instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead { x // p x } α wh
 /-
   Remark: one may question why we use `OfNat α` instead of `Coe Nat α`.
   Reason: `OfNat` is for implementing polymorphic numeric literals, and we may
-  want to have numberic literals for a type α and **no** coercion from `Nat` to `α`. -/
+  want to have numeric literals for a type α and **no** coercion from `Nat` to `α`. -/
 instance hasOfNatOfCoe [Coe α β] [OfNat α n] : OfNat β n where
   ofNat := coe (OfNat.ofNat n : α)