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

fix(kernel/default_converter): use is_opaque at is_delta

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-07 17:30:36 -08:00
parent b4f1029318
commit 7823905fc1
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/kernel/default_converter.cpp
View file

@ -158,7 +158,13 @@ expr default_converter::unfold_names(expr const & e, unsigned w) {
to be expanded.
*/
optional<declaration> default_converter::is_delta(expr const & e) {
return ::lean::is_delta(m_env, get_app_fn(e), m_extra_pred, m_module_idx);
expr const & f = get_app_fn(e);
if (is_constant(f)) {
if (auto d = m_env.find(const_name(f)))
if (d->is_definition() && !is_opaque(*d))
return d;
}
return none_declaration();
}
/**