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

feat(kernel/converter): relax is_def_eq test for local constants and meta-variables

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-14 15:31:57 -07:00
parent 940092a975
commit de7c850782
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/kernel/converter.cpp
View file

@ -548,8 +548,7 @@ struct default_converter : public converter {
is_def_eq(const_levels(t_n), const_levels(s_n), c, jst, cs)) is_def_eq(const_levels(t_n), const_levels(s_n), c, jst, cs))
return to_bcs(true, cs); return to_bcs(true, cs);
if (is_local(t_n) && is_local(s_n) && mlocal_name(t_n) == mlocal_name(s_n) && if (is_local(t_n) && is_local(s_n) && mlocal_name(t_n) == mlocal_name(s_n))
is_def_eq(mlocal_type(t_n), mlocal_type(s_n), c, jst, cs))
return to_bcs(true, cs); return to_bcs(true, cs);
optional<declaration> d_t, d_s; optional<declaration> d_t, d_s;