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

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

diff --git a/library/Init/Lean/Meta/InferType.lean b/library/Init/Lean/Meta/InferType.lean
index dbdc6e3e25..e3cc4d98e8 100644
--- a/library/Init/Lean/Meta/InferType.lean
+++ b/library/Init/Lean/Meta/InferType.lean
@@ -37,9 +37,9 @@ do env ← getEnv;
    match env.find c with
    | some cinfo =>
      if cinfo.lparams.length == lvls.length then
-       throwEx $ Exception.incorrectNumOfLevels c lvls
-     else
        pure $ cinfo.instantiateTypeLevelParams lvls
+     else
+       throwEx $ Exception.incorrectNumOfLevels c lvls
    | none =>
      throwEx $ Exception.unknownConst c