From 88fc24c58c72aab019ed7a6e2513d0e5ef94de08 Mon Sep 17 00:00:00 2001
From: Yuri de Wit <ydewit@gmail.com>
Date: Mon, 19 Sep 2022 10:27:35 -0300
Subject: [PATCH] chore: fixed typos

---
 src/Lean/Expr.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 53f62059ed..9982dbaeba 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -292,7 +292,7 @@ instance : Inhabited (MVarIdMap α) where
 
 /--
 Lean expressions. This datastructure is used in the kernel and
-elaborator. Howewer, expressions sent to the kernel should not
+elaborator. However, expressions sent to the kernel should not
 contain metavariables.
 
 Remark: we use the `E` suffix (short for `Expr`) to avoid collision with keywords.
@@ -338,7 +338,7 @@ inductive Expr where
   /--
   A (universe polymorphic) constant. For example,
   `@Eq.{1}` is represented as ``.const `Eq [.succ .zero]``, and
-  `@Array.map.{0, 0}` is represented as ``.cons `Array.map [.zero, .zero]``.
+  `@Array.map.{0, 0}` is represented as ``.const `Array.map [.zero, .zero]``.
   -/
   | const (declName : Name) (us : List Level)
   /--