michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(kernel/type_checker): avoid assertion violation due to API misuse

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-15 14:17:34 -07:00
parent 90c4957071
commit 16553e77fa
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/kernel/type_checker.cpp
View file

@ -276,6 +276,9 @@ struct type_checker::imp {
\pre closed(e) \pre closed(e)
*/ */
expr infer_type_core(expr const & e, bool infer_only) { expr infer_type_core(expr const & e, bool infer_only) {
if (is_var(e))
throw_kernel_exception(m_env, "type checker does not support free variables, replace them with local constants before invoking it", e);
lean_assert(closed(e)); lean_assert(closed(e));
check_system("type checker"); check_system("type checker");
@ -291,7 +294,7 @@ struct type_checker::imp {
r = mlocal_type(e); r = mlocal_type(e);
break; break;
case expr_kind::Var: case expr_kind::Var:
throw_kernel_exception(m_env, "type checker does not support free variables, replace them with local constants before invoking it", e); lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Sort: case expr_kind::Sort:
if (!infer_only) if (!infer_only)
check_level(sort_level(e), e); check_level(sort_level(e), e);