max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: typo

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-21 11:23:46 -08:00
parent 7c7849422f
commit 100664cb39
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/Init/Lean/Meta/Check.lean
View file

@ -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)