diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 44fc50ede..63b135d97 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -583,6 +583,9 @@ template expr update_eq(expr const & e, F f) { return e; } template expr update_metavar(expr const & e, unsigned i, F f) { + static_assert(std::is_same::type, + meta_entry>::value, + "update_metavar: return type of f(meta_entry) is not meta_entry"); buffer new_entries; bool modified = (i != metavar_idx(e)); for (meta_entry const & me : metavar_ctx(e)) { @@ -603,6 +606,9 @@ template expr update_metavar(expr const & e, unsigned i, F f) { return e; } template expr update_metavar(expr const & e, F f) { + static_assert(std::is_same::type, + meta_entry>::value, + "update_metavar: return type of f(meta_entry) is not meta_entry"); return update_metavar(e, metavar_idx(e), f); } // ======================================= diff --git a/src/kernel/expr_eq.h b/src/kernel/expr_eq.h index 5a02036f6..9c9244fcb 100644 --- a/src/kernel/expr_eq.h +++ b/src/kernel/expr_eq.h @@ -71,7 +71,12 @@ class expr_eq_fn { lean_unreachable(); } public: - expr_eq_fn(N const & norm = N()):m_norm(norm) {} + expr_eq_fn(N const & norm = N()):m_norm(norm) { + // the return type of N()(e) should be expr const & + static_assert(std::is_same())(expr const &)>::type, + expr const &>::value, + "The return type of CMP()(k1, k2) is not int."); + } bool operator()(expr const & a, expr const & b) { return apply(a, b); } diff --git a/src/kernel/replace.h b/src/kernel/replace.h index 1b866a126..e972e56a1 100644 --- a/src/kernel/replace.h +++ b/src/kernel/replace.h @@ -36,6 +36,11 @@ template class replace_fn { static_assert(std::is_same::type, expr>::value, "replace_fn: return type of F is not expr"); + // the return type of P()(e1, e2) should be void + static_assert(std::is_same())(expr const &, expr const &)>::type, + void>::value, + "The return type of P()(e1, e2) is not void"); + expr_cell_offset_map m_cache; F m_f; P m_post;