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

fix(kernel/inductive): use has_expr_metavar_strict instead of has_expr_metavar

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-26 19:57:54 -07:00
parent 5c5dea7c8e
commit cb232f2a9b
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/inductive/inductive.cpp
View file

@ -823,7 +823,7 @@ bool is_elim_meta_app_core(Ctx & ctx, expr const & e) {
if (elim_args.size() < major_idx + 1)
return false;
expr intro_app = ctx.whnf(elim_args[major_idx]);
return has_expr_metavar(intro_app);
return has_expr_metavar_strict(intro_app);
}
bool is_elim_meta_app(type_checker & tc, expr const & e) {

2
src/library/inductive_unifier_plugin.cpp
View file

@ -52,7 +52,7 @@ class inductive_unifier_plugin_cell : public unifier_plugin_cell {
unsigned elim_num_lvls = length(elim_lvls);
unsigned major_idx = *inductive::get_elim_major_idx(env, const_name(elim));
expr meta = args[major_idx]; // save this argument, we will update it
lean_assert(has_expr_metavar(meta));
lean_assert(has_expr_metavar_strict(meta));
buffer<expr> margs;
expr const & m = get_app_args(meta, margs);
expr mtype = tc.infer(m, tc_cnstr_buffer);