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

chore(frontends/lean/placeholder_elaborator): indent code

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-04 10:36:10 -07:00
parent 0a288aec40
commit a9741c5c30
1 changed files with 14 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/frontends/lean/placeholder_elaborator.cpp
View file

@ -273,9 +273,9 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr<placeholder_context> const
return lazy_list<constraints>(constraints()); return lazy_list<constraints>(constraints());
} }
pair<expr, justification> mj = update_meta(meta, s); pair<expr, justification> mj = update_meta(meta, s);
expr new_meta = mj.first; expr new_meta = mj.first;
justification new_j = mj.second; justification new_j = mj.second;
constraint c = mk_placeholder_cnstr(C, new_meta); constraint c = mk_placeholder_cnstr(C, new_meta);
unifier_config new_cfg(cfg); unifier_config new_cfg(cfg);
new_cfg.m_discard = false; new_cfg.m_discard = false;
new_cfg.m_use_exceptions = false; new_cfg.m_use_exceptions = false;
@ -288,17 +288,17 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr<placeholder_context> const
}); });
lazy_list<constraints> seq3 = map2<constraints>(seq2, [=](pair<substitution, constraints> const & p) { lazy_list<constraints> seq3 = map2<constraints>(seq2, [=](pair<substitution, constraints> const & p) {
substitution new_s = p.first; substitution new_s = p.first;
// some constraints may have been postponed (example: universe level constraints) // some constraints may have been postponed (example: universe level constraints)
constraints postponed = map(p.second, constraints postponed = map(p.second,
[&](constraint const & c) { [&](constraint const & c) {
// we erase internal justifications // we erase internal justifications
return update_justification(c, new_j); return update_justification(c, mk_composite1(j, new_j));
}); });
metavar_closure cls(new_meta); metavar_closure cls(new_meta);
cls.add(meta_type); cls.add(meta_type);
bool relax = C->m_relax; bool relax = C->m_relax;
constraints cs = cls.mk_constraints(new_s, new_j, relax); constraints cs = cls.mk_constraints(new_s, new_j, relax);
return append(cs, postponed); return append(cs, postponed);
}); });
if (is_strict) { if (is_strict) {
return seq3; return seq3;