From 100664cb3943b3f242546a3f0a2950638fc21e7e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Nov 2019 11:23:46 -0800 Subject: [PATCH] fix: typo --- library/Init/Lean/Meta/Check.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/Init/Lean/Meta/Check.lean b/library/Init/Lean/Meta/Check.lean index afd11bdec0..f835f03c82 100644 --- a/library/Init/Lean/Meta/Check.lean +++ b/library/Init/Lean/Meta/Check.lean @@ -52,7 +52,7 @@ private def checkConstant (c : Name) (lvls : List Level) : MetaM Unit := do env ← getEnv; match env.find c with | none => throwEx $ Exception.unknownConst c - | some cinfo => unless (lvls.length != cinfo.lparams.length) $ throwEx $ Exception.incorrectNumOfLevels c lvls + | some cinfo => unless (lvls.length == cinfo.lparams.length) $ throwEx $ Exception.incorrectNumOfLevels c lvls @[specialize] private def checkApp (check : Expr → MetaM Unit)