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

fix(library/unification_hint): unification hint pp

Browse source
This commit is contained in:
Leonardo de Moura 2016-03-09 12:52:28 -08:00
parent a823b0e6ec
commit 6caca44e41
2 changed files with 12 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/library/unification_hint.cpp
View file

@ -193,10 +193,15 @@ format unification_hint::pp(unsigned prio, formatter const & fmt) const {
format r1 = fmt(get_lhs()) + space() + format("=?=") + pp_indent_expr(fmt, get_rhs());
r1 += space() + lcurly();
r += group(r1);
for_each(m_constraints, [&](expr_pair p) {
r += fmt(p.first) + space() + format("=?=");
r += space() + fmt(p.second) + comma() + space();
});
bool first = true;
for (expr_pair const & p : m_constraints) {
if (first) {
first = false;
} else {
r += comma() + space();
}
r += fmt(p.first) + space() + format("=?=") + space() + fmt(p.second);
}
r += rcurly();
return r;
}

7
tests/lean/unification_hints1.lean.expected.out
View file

@ -5,11 +5,10 @@ unification hints:
fail
success
unification hints:
(add, nat.succ) #4 + 1 =?= succ #3 {#4 =?= #3, }
(add, nat.succ) #4 + 1 =?= succ #3 {#4 =?= #3}
fail
success
unification hints:
(canonical.Canonical.carrier, canonical.A) Canonical.carrier #0 =?= A {#0 =?= A_canonical, }
(canonical.Canonical.carrier, canonical.A) Canonical.carrier #0 =?= A {#0 =?= A_canonical}
unification hints at namespace 'canonical':
(canonical.Canonical.carrier, canonical.A) canonical.Canonical.carrier #0 =?=
canonical.A {#0 =?= canonical.A_canonical, }
(canonical.Canonical.carrier, canonical.A) canonical.Canonical.carrier #0 =?= canonical.A {#0 =?= canonical.A_canonical}