diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index ef3950a40..f128646b6 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -131,7 +131,9 @@ expr_app::expr_app(expr const & fn, expr const & arg): fn.has_param_univ() || arg.has_param_univ(), std::max(get_depth(fn), get_depth(arg)) + 1, std::max(get_free_var_range(fn), get_free_var_range(arg))), - m_fn(fn), m_arg(arg) {} + m_fn(fn), m_arg(arg) { + m_hash = ::lean::hash(m_hash, m_depth); +} void expr_app::dealloc(buffer & todelete) { dec_ref(m_fn, todelete); dec_ref(m_arg, todelete); diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 4cb654fe3..bf0e496a5 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -214,6 +214,7 @@ public: /** \brief Composite expressions */ class expr_composite : public expr_cell { +protected: unsigned m_depth; unsigned m_free_var_range; friend unsigned get_depth(expr const & e);