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

fix(library/proof_irrel_expr_manager): add missing Let case

Browse source
This commit is contained in:
Leonardo de Moura 2016-03-01 14:27:37 -08:00
parent 1104537d02
commit 16dc021736
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/proof_irrel_expr_manager.cpp
View file

@ -20,6 +20,9 @@ unsigned proof_irrel_expr_manager::hash(expr const & e) {
case expr_kind::Var: case expr_kind::Var:
case expr_kind::Macro: case expr_kind::Macro:
return e.hash(); return e.hash();
case expr_kind::Let:
// Let-expressions must be unfolded before invoking this method
lean_unreachable();
case expr_kind::Lambda: case expr_kind::Lambda:
case expr_kind::Pi: case expr_kind::Pi:
h = hash(binding_domain(e)); h = hash(binding_domain(e));
@ -67,6 +70,9 @@ bool proof_irrel_expr_manager::is_equal(expr const & a, expr const & b) {
return a == b; return a == b;
case expr_kind::Meta: case expr_kind::Local: case expr_kind::Meta: case expr_kind::Local:
return mlocal_name(a) == mlocal_name(b) && is_equal(mlocal_type(a), mlocal_type(b)); return mlocal_name(a) == mlocal_name(b) && is_equal(mlocal_type(a), mlocal_type(b));
case expr_kind::Let:
// Let-expressions must be unfolded before invoking this method
lean_unreachable();
case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Lambda: case expr_kind::Pi:
if (!is_equal(binding_domain(a), binding_domain(b))) return false; if (!is_equal(binding_domain(a), binding_domain(b))) return false;
// see comment at proof_irrel_expr_manager::hash // see comment at proof_irrel_expr_manager::hash