From 2ada3af4055f2c9b98f2e8aaee007644507f0c61 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 22 Aug 2014 15:55:15 -0700 Subject: [PATCH] fix(frontends/lean/info_manager): add instantiate method to synth_info_data, fixes #94 Signed-off-by: Leonardo de Moura --- src/frontends/lean/info_manager.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index 6e9632997..142cdec19 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -78,9 +78,7 @@ public: type_info_data() {} type_info_data(unsigned c, expr const & e):info_data_cell(c), m_expr(e) {} - expr const & get_type() const { - return m_expr; - } + expr const & get_type() const { return m_expr; } virtual void display(io_state_stream const & ios, unsigned line) const { ios << "-- TYPE|" << line << "|" << get_column() << "\n"; @@ -90,10 +88,7 @@ public: virtual info_data_cell * instantiate(substitution & s) const { expr e = s.instantiate(m_expr); - if (is_eqp(e, m_expr)) - return nullptr; - else - return new type_info_data(get_column(), e); + return is_eqp(e, m_expr) ? nullptr : new type_info_data(get_column(), e); } }; @@ -105,6 +100,11 @@ public: ios << m_expr << endl; ios << "-- ACK" << endl; } + + virtual info_data_cell * instantiate(substitution & s) const { + expr e = s.instantiate(m_expr); + return is_eqp(e, m_expr) ? nullptr : new synth_info_data(get_column(), e); + } }; class overload_info_data : public info_data_cell {