From e76a2a6d9eab9e9fe2b96ac5fa23a3ed725580a9 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 3 May 2022 10:25:42 +0200
Subject: [PATCH] chore: normalize spelling

---
 src/Lean/Elab/Term.lean                          | 2 +-
 tests/lean/mulcommErrorMessage.lean.expected.out | 4 ++--
 tests/lean/run/meta.lean                         | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 48cedfed52..ca468f960d 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1196,7 +1196,7 @@ private def decorateErrorMessageWithLambdaImplicitVars (ex : Exception) (impFVar
     if impFVars.isEmpty then
       return Exception.error ref msg
     else
-      let mut msg := m!"{msg}\nthe following variables have been introduced by the implicit lamda feature"
+      let mut msg := m!"{msg}\nthe following variables have been introduced by the implicit lambda feature"
       for impFVar in impFVars do
         let auxMsg := m!"{impFVar} : {← inferType impFVar}"
         let auxMsg ← addMessageContext auxMsg
diff --git a/tests/lean/mulcommErrorMessage.lean.expected.out b/tests/lean/mulcommErrorMessage.lean.expected.out
index a3e3749dc2..638fb3b4b2 100644
--- a/tests/lean/mulcommErrorMessage.lean.expected.out
+++ b/tests/lean/mulcommErrorMessage.lean.expected.out
@@ -4,7 +4,7 @@ has type
   (a : ?m) → (b : ?m a) → ?m a b : Sort (imax ?u ?u ?u)
 but is expected to have type
   a✝ * b✝ = b✝ * a✝ : Prop
-the following variables have been introduced by the implicit lamda feature
+the following variables have been introduced by the implicit lambda feature
   a✝ : Bool
   b✝ : Bool
 you can disable implict lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.
@@ -20,7 +20,7 @@ has type
   (a b : Bool) → ?m a b a : Sort (imax 1 1 ?u)
 but is expected to have type
   a✝ * b✝ = b✝ * a✝ : Prop
-the following variables have been introduced by the implicit lamda feature
+the following variables have been introduced by the implicit lambda feature
   a✝ : Bool
   b✝ : Bool
 you can disable implict lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.
diff --git a/tests/lean/run/meta.lean b/tests/lean/run/meta.lean
index 15a2899cfc..b2451c5650 100644
--- a/tests/lean/run/meta.lean
+++ b/tests/lean/run/meta.lean
@@ -21,7 +21,7 @@ def mkLam1 : MetaM Expr :=
     -- Double backticks instruct Lean to resolve the names at compilation time
     let b ← mkAppM ``HAdd.hAdd #[x, y] -- `x + y`
     let b ← mkAppM ``HAdd.hAdd #[b, x] -- `x + y + x`
-    /- `mkLamdaFVars` converts the free variables into de-Bruijn bound variables, and construct the lambda for us. -/
+    /- `mkLambdaFVars` converts the free variables into de-Bruijn bound variables, and construct the lambda for us. -/
     mkLambdaFVars #[x, y] b
 
 #eval execShow mkLam1