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

refactor(kernel): simplify expr_eq

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-25 22:09:08 -07:00
parent 23e2f72f42
commit 98b4e09063
1 changed files with 1 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/kernel/expr_eq.h
View file

@ -56,14 +56,7 @@ class expr_eq_fn {
case expr_kind::Pi: return apply(abst_domain(a), abst_domain(b)) && apply(abst_body(a), abst_body(b));
case expr_kind::Type: return ty_level(a) == ty_level(b);
case expr_kind::Value: return to_value(a) == to_value(b);
case expr_kind::Let:
if (let_type(a) && let_type(b)) {
if (!apply(let_type(a), let_type(b)))
return false;
} else if (let_type(a) || let_type(b)) {
return false;
}
return apply(let_value(a), let_value(b)) && apply(let_body(a), let_body(b));
case expr_kind::Let: return apply(let_type(a), let_type(b)) && apply(let_value(a), let_value(b)) && apply(let_body(a), let_body(b));
case expr_kind::MetaVar:
return metavar_idx(a) == metavar_idx(b) &&
compare(metavar_ctx(a), metavar_ctx(b), [&](meta_entry const & e1, meta_entry const & e2) {