max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/tactic/congruence/congruence_closure): fix typo

Browse source
This commit is contained in:
Leonardo de Moura 2016-12-22 19:13:15 -08:00
parent 77737a621d
commit 6329afc121
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/tactic/congruence/congruence_closure.cpp
View file

@ -1287,10 +1287,10 @@ format congruence_closure::state::pp_eqcs(formatter const & fmt) const {
format r;
bool first = true;
for (expr const & root : roots) {
if (first) first = false; r += line();
if (first) first = false; else r += comma() + line();
r += pp_eqc(fmt, root);
}
return r;
return bracket("{", group(r), "}");
}
void initialize_congruence_closure() {