From cfcbb6e9dc2f959159418ac8be746da5c40d65b4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 11 Nov 2019 09:16:28 -0800
Subject: [PATCH] fix: typo

---
 library/Init/Lean/Meta/InferType.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/library/Init/Lean/Meta/InferType.lean b/library/Init/Lean/Meta/InferType.lean
index f944a4dc8a..88a8722bff 100644
--- a/library/Init/Lean/Meta/InferType.lean
+++ b/library/Init/Lean/Meta/InferType.lean
@@ -100,8 +100,7 @@ do typeType ← inferType type;
     (inferType : Expr → MetaM Expr)
     (e : Expr) : MetaM Expr :=
 forallTelescope whnf e $ fun xs e => do
-  type ← inferType e;
-  lvl  ← getLevel whnf inferType type;
+  lvl  ← getLevel whnf inferType e;
   lvl  ← xs.foldrM
     (fun x lvl => do
       xType    ← inferType x;