michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

style(library/blast/simplifier): whitespace

Browse source
This commit is contained in:
Daniel Selsam 2015-11-07 17:12:34 -08:00 committed by Leonardo de Moura
parent 30b2bcbea6
commit b2368ba81b
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/blast/simplifier.cpp
View file

@ -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)) {