diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 589982c8b..374d74153 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -587,6 +587,8 @@ template expr update_eq(expr const & e, F f) { return e; } template expr update_metavar(expr const & e, name const & n, F f) { + static_assert(std::is_same::type, local_entry>::value, + "update_metavar: return type of f(local_entry) is not local_entry"); buffer new_entries; bool modified = n != metavar_name(e); for (local_entry const & me : metavar_lctx(e)) { @@ -607,6 +609,8 @@ template expr update_metavar(expr const & e, name const & n, F f) { return e; } template expr update_metavar(expr const & e, F f) { + static_assert(std::is_same::type, local_entry>::value, + "update_metavar: return type of f(local_entry) is not local_entry"); return update_metavar(e, metavar_name(e), f); } inline expr update_metavar(expr const & e, local_context const & lctx) {