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

fix(kernel/type_checker): add missing test: number of universe level parameters

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-12 12:57:27 -07:00
parent 6f03064c46
commit 1244a951f2
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/kernel/type_checker.cpp
View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include "util/interrupt.h" #include "util/interrupt.h"
#include "util/lbool.h" #include "util/lbool.h"
#include "util/flet.h" #include "util/flet.h"
#include "util/sstream.h"
#include "kernel/type_checker.h" #include "kernel/type_checker.h"
#include "kernel/expr_maps.h" #include "kernel/expr_maps.h"
#include "kernel/instantiate.h" #include "kernel/instantiate.h"
@ -326,6 +327,9 @@ struct type_checker::imp {
definition d = m_env.get(const_name(e)); definition d = m_env.get(const_name(e));
auto const & ps = d.get_params(); auto const & ps = d.get_params();
auto const & ls = const_level_params(e); auto const & ls = const_level_params(e);
if (length(ps) != length(ls))
throw_kernel_exception(m_env, sstream() << "incorrect number of universe levels parameters for '" << const_name(e) << "', #"
<< length(ps) << " expected, #" << length(ls) << " provided");
r = instantiate_params(d.get_type(), ps, ls); r = instantiate_params(d.get_type(), ps, ls);
break; break;
} }