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

chore(kernel/old_type_checker): fix test

Browse source
This commit is contained in:
Leonardo de Moura 2018-06-22 14:39:46 -07:00
parent f809758dd3
commit a18c508f5c
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/old_type_checker.cpp
View file

@ -204,7 +204,7 @@ expr old_type_checker::infer_type_core(expr const & e, bool infer_only) {
expr r;
switch (e.kind()) {
case expr_kind::FVar: r = local_type(e); break;
case expr_kind::MVar: throw kernel_exception(m_env, "kernel type checker does not support meta variables");
case expr_kind::MVar: r = mvar_type(e); break;
case expr_kind::BVar:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Sort: