fix: typo

2019-11-11 08:47:00 -08:00 · 2019-11-11 08:47:00 -08:00 · b4cc85e92d
commit b4cc85e92d
parent b771ec7328
1 changed files with 2 additions and 2 deletions
--- 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