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

feat(kernel/metavar): add additional assertions

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-20 17:46:06 -07:00
parent eb23a30626
commit 47e37a3353
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/kernel/metavar.cpp
View file

@ -60,11 +60,13 @@ optional<level> substitution::get_level(name const & m) const {
}
void substitution::assign(expr const & mvar, buffer<expr> const & locals, expr const & v, justification const & j) {
lean_assert(mvar != v);
assign(mlocal_name(mvar), Fun(locals, v), j);
}
void substitution::assign(name const & m, expr const & t, justification const & j) {
lean_assert(closed(t));
lean_assert(!is_metavar(t) || m != mlocal_name(t));
m_expr_subst.insert(m, t);
m_occs_map.erase(m);
if (!j.is_none())
@ -270,6 +272,7 @@ auto substitution::expand_metavar_app(expr const & e) -> opt_expr_jst {
return opt_expr_jst();
buffer<expr> args;
get_app_rev_args(e, args);
lean_assert(*f_value != f);
expr new_e = apply_beta(*f_value, args.size(), args.data());
return opt_expr_jst(new_e, get_expr_jst(f_name));
}