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

fix(library/coercion): bug in add_coercion_trans

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-25 06:25:31 -07:00
parent 6536232107
commit 1ee6bb48fc
1 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/library/coercion.cpp
View file

@ -146,16 +146,18 @@ static void add_coercion_trans(coercion_ext & ext, io_state const & ios, name co
level_param_names const & f_level_params, expr const & f, expr const & f_type, unsigned f_num_args, level_param_names const & f_level_params, expr const & f, expr const & f_type, unsigned f_num_args,
level_param_names const & g_level_params, expr g, expr const & g_type, unsigned g_num_args) { level_param_names const & g_level_params, expr g, expr const & g_type, unsigned g_num_args) {
expr t = f_type; expr t = f_type;
buffer<name> f_arg_names;
buffer<expr> f_arg_types;
buffer<expr> args; buffer<expr> args;
unsigned i = f_num_args; unsigned i = f_num_args;
while (i > 0) {
i--;
args.push_back(mk_var(i));
}
buffer<name> f_arg_names;
buffer<expr> f_arg_types;
while (is_pi(t)) { while (is_pi(t)) {
f_arg_names.push_back(binding_name(t)); f_arg_names.push_back(binding_name(t));
f_arg_types.push_back(binding_domain(t)); f_arg_types.push_back(binding_domain(t));
t = binding_body(t); t = binding_body(t);
i--;
args.push_back(mk_var(i));
} }
expr f_app = apply_beta(f, args.size(), args.data()); expr f_app = apply_beta(f, args.size(), args.data());
expr D_app = t; expr D_app = t;