diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 83346152f1..434a49bf42 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -149,7 +149,7 @@ void expr_app::dealloc(buffer & todelete) { // Expr binders (Lambda, Pi and Sigma) expr_binder::expr_binder(expr_kind k, name const & n, expr const & t, expr const & b): expr_composite(k, ::lean::hash(t.hash(), b.hash()), t.has_metavar() || b.has_metavar(), - std::max(get_depth(m_domain), get_depth(m_body)) + 1), + std::max(get_depth(t), get_depth(b)) + 1), m_name(n), m_domain(t), m_body(b) { diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp index 65eafe0abf..010cdabf3d 100644 --- a/src/kernel/instantiate.cpp +++ b/src/kernel/instantiate.cpp @@ -93,7 +93,7 @@ expr head_beta_reduce(expr const & t) { expr const * it = &t; while (true) { lean_assert(is_app(*it)); - expr f = app_fn(*it); + expr const & f = app_fn(*it); args.push_back(app_arg(*it)); if (is_lambda(f)) { return apply_beta(f, args.size(), args.data());