From ccc09d9cbf5f0b0128073d92c9bb756904843206 Mon Sep 17 00:00:00 2001
From: Reid Barton <rwbarton@gmail.com>
Date: Mon, 25 Jan 2021 16:51:59 -0500
Subject: [PATCH] chore: fix typo

invalide -> invalid
---
 src/Lean/Meta/InferType.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean
index 261b96fc49..0965a12743 100644
--- a/src/Lean/Meta/InferType.lean
+++ b/src/Lean/Meta/InferType.lean
@@ -95,7 +95,7 @@ private def inferConstType (c : Name) (us : List Level) : MetaM Expr := do
 
 private def inferProjType (structName : Name) (idx : Nat) (e : Expr) : MetaM Expr := do
   let failed {α} : Unit → MetaM α := fun _ =>
-    throwError! "invalide projection{indentExpr (mkProj structName idx e)}"
+    throwError! "invalid projection{indentExpr (mkProj structName idx e)}"
   let structType ← inferType e
   let structType ← whnf structType
   matchConstStruct structType.getAppFn failed fun structVal structLvls ctorVal =>