From b2368ba81b5cbf2c7421f0bbdf9f6f9314ed2b6d Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Sat, 7 Nov 2015 17:12:34 -0800 Subject: [PATCH] style(library/blast/simplifier): whitespace --- src/library/blast/simplifier.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/library/blast/simplifier.cpp b/src/library/blast/simplifier.cpp index f5806a833..8f6415c63 100644 --- a/src/library/blast/simplifier.cpp +++ b/src/library/blast/simplifier.cpp @@ -407,7 +407,7 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) { blast_tmp_type_context tmp_tctx(sr.get_num_umeta(), sr.get_num_emeta()); if (!tmp_tctx->is_def_eq(e, sr.get_lhs())) return result(e); - + if (m_trace) { expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sr.get_lhs()); expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs()); @@ -423,7 +423,7 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) { expr m_type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m)); lean_assert(!has_metavar(m_type)); - + if (is_instance) { if (auto v = tmp_tctx->mk_class_instance(m_type)) { if (!tmp_tctx->force_assign(m, *v)) {