From e39a6e732adfd7633f60c218e35eedaf6687e1ec Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 19 Jul 2014 21:15:32 +0100 Subject: [PATCH] refactor(kernel/error_msgs): move pp_type_mismatch to error_msgs module Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 8 -------- src/kernel/error_msgs.cpp | 8 ++++++++ src/kernel/error_msgs.h | 1 + 3 files changed, 9 insertions(+), 8 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index b436402f6..60e4cd47e 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1153,14 +1153,6 @@ public: return apply(s, r); } - static format pp_type_mismatch(formatter const & fmt, expr const & expected_type, expr const & given_type) { - format r("type mismatch, expected type"); - r += ::lean::pp_indent_expr(fmt, expected_type); - r += compose(line(), format("given type:")); - r += ::lean::pp_indent_expr(fmt, given_type); - return r; - } - std::tuple operator()(expr const & t, expr const & v, name const & n) { lean_assert(!has_local(t)); lean_assert(!has_local(v)); expr r_t = ensure_type(visit(t)); diff --git a/src/kernel/error_msgs.cpp b/src/kernel/error_msgs.cpp index 10863f6b8..d57702eec 100644 --- a/src/kernel/error_msgs.cpp +++ b/src/kernel/error_msgs.cpp @@ -40,6 +40,14 @@ format pp_def_type_mismatch(formatter const & fmt, name const & n, expr const & return r; } +format pp_type_mismatch(formatter const & fmt, expr const & expected_type, expr const & given_type) { + format r("type mismatch, expected type"); + r += ::lean::pp_indent_expr(fmt, expected_type); + r += compose(line(), format("given type:")); + r += ::lean::pp_indent_expr(fmt, given_type); + return r; +} + format pp_decl_has_metavars(formatter const & fmt, name const & n, expr const & e, bool is_type) { format r("failed to add declaration '"); r += format(n); diff --git a/src/kernel/error_msgs.h b/src/kernel/error_msgs.h index 8d6cf15a0..16daac504 100644 --- a/src/kernel/error_msgs.h +++ b/src/kernel/error_msgs.h @@ -13,5 +13,6 @@ format pp_type_expected(formatter const & fmt, expr const & e); format pp_function_expected(formatter const & fmt, expr const & e); format pp_app_type_mismatch(formatter const & fmt, expr const & app, expr const & expected_type, expr const & given_type); format pp_def_type_mismatch(formatter const & fmt, name const & n, expr const & expected_type, expr const & given_type); +format pp_type_mismatch(formatter const & fmt, expr const & expected_type, expr const & given_type); format pp_decl_has_metavars(formatter const & fmt, name const & n, expr const & e, bool is_type); }