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

fix(library/blast/blast): temporary type_context for blast must handle external meta-variables.

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-02 13:37:48 -08:00
parent dc203b28db
commit 5b71025b07
1 changed files with 13 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/library/blast/blast.cpp
View file

@ -145,6 +145,8 @@ class blastenv {
} }
virtual expr infer_metavar(expr const & m) const { virtual expr infer_metavar(expr const & m) const {
// Remark: we do not tolerate external meta-variables here.
lean_assert(is_mref(m));
state const & s = m_benv.m_curr_state; state const & s = m_benv.m_curr_state;
metavar_decl const * d = s.get_metavar_decl(m); metavar_decl const * d = s.get_metavar_decl(m);
lean_assert(d); lean_assert(d);
@ -558,10 +560,17 @@ public:
} }
virtual expr infer_metavar(expr const & m) const { virtual expr infer_metavar(expr const & m) const {
state const & s = curr_state(); if (is_mref(m)) {
metavar_decl const * d = s.get_metavar_decl(m); state const & s = curr_state();
lean_assert(d); metavar_decl const * d = s.get_metavar_decl(m);
return d->get_type(); lean_assert(d);
return d->get_type();
} else {
// The type of external meta-variables is encoded in the usual way.
// In temporary type_context objects, we may have temporary meta-variables
// created by external modules (e.g., simplifier and app_builder).
return mlocal_type(m);
}
} }
}; };