From 02fc447b047850e7223e2a1c824bfb4fe382abcd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 9 Sep 2020 16:42:41 -0700
Subject: [PATCH] fix: error message

---
 src/Lean/Meta/Check.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index a36c6ccff6..bbaa127965 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -19,7 +19,7 @@ _ ← getLevel e; pure ()
 def throwLetTypeMismatchMessage {α} (fvarId : FVarId) : MetaM α := do
 lctx ← getLCtx;
 match lctx.find? fvarId with
-| some (LocalDecl.ldecl _ n t v b _) => do
+| some (LocalDecl.ldecl _ _ n t v _) => do
   vType ← inferType v;
   throwError $
      "invalid let declaration, term" ++ indentExpr v