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

fix(frontends/lean/pp): bug in pp arrow

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-31 11:01:21 -07:00
parent ca110012d8
commit 55608c9b9f
3 changed files with 22 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/pp.cpp
View file

@ -709,7 +709,7 @@ auto pretty_fn::pp_pi(expr const & e) -> result {
result lhs = pp_child(binding_domain(e), get_arrow_prec()); result lhs = pp_child(binding_domain(e), get_arrow_prec());
result rhs = pp_child(lift_free_vars(binding_body(e), 1), get_arrow_prec()-1); result rhs = pp_child(lift_free_vars(binding_body(e), 1), get_arrow_prec()-1);
format r = group(lhs.fmt() + space() + (m_unicode ? *g_arrow_n_fmt : *g_arrow_fmt) + line() + rhs.fmt()); format r = group(lhs.fmt() + space() + (m_unicode ? *g_arrow_n_fmt : *g_arrow_fmt) + line() + rhs.fmt());
return result(get_arrow_prec()-1, r); return result(get_arrow_prec(), get_arrow_prec()-1, r);
} else { } else {
expr b = e; expr b = e;
buffer<expr> locals; buffer<expr> locals;

11
tests/lean/pp_bug.lean Normal file
View file

@ -0,0 +1,11 @@
variables p q : Prop
check ¬(p → q)
check ¬p → q
check (¬p) → q
check ¬(p → q)
check p ↔ q
check ¬(p ↔ q)
check ¬p ↔ q
check (¬p) ↔ q
check (p → q) ↔ q
check p → (q ↔ q)

10
tests/lean/pp_bug.lean.expected.out Normal file
View file

@ -0,0 +1,10 @@
¬(p → q) : Prop
¬p → q : Prop
¬p → q : Prop
¬(p → q) : Prop
p ↔ q : Prop
¬(p ↔ q) : Prop
¬p ↔ q : Prop
¬p ↔ q : Prop
p → q ↔ q : Prop
p → (q ↔ q) : Prop