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

fix(frontends/lean/pp): implicit arguments in notation

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-19 09:04:43 -07:00
parent 85339c0cc1
commit eef1cc4ac2
3 changed files with 11 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -653,12 +653,12 @@ static unsigned get_some_precedence(token_table const & t, name const & tk) {
} }
auto pretty_fn::pp_notation_child(expr const & e, unsigned lbp, unsigned rbp) -> result { auto pretty_fn::pp_notation_child(expr const & e, unsigned lbp, unsigned rbp) -> result {
if (is_app(e) && !m_coercion && is_coercion(m_env, get_app_fn(e))) { if (is_app(e) && is_implicit(app_fn(e))) {
return pp_notation_child(app_fn(e), lbp, rbp);
} else if (is_app(e) && !m_coercion && is_coercion(m_env, get_app_fn(e))) {
return pp_coercion(e, rbp); return pp_coercion(e, rbp);
} else { } else {
result r = pp(e); result r = pp(e);
// std::cout << "e: " << e << "\n";
// std::cout << "lbp: " << lbp << ", rbp: " << rbp << ", r.lbp(): " << r.lbp() << ", r.rbp(): " << r.rbp() << "\n\n";
if (r.rbp() < lbp || r.lbp() <= rbp) { if (r.rbp() < lbp || r.lbp() <= rbp) {
return result(paren(r.fmt())); return result(paren(r.fmt()));
} else { } else {

5
tests/lean/notation2.lean Normal file
View file

@ -0,0 +1,5 @@
import data.list data.num
open list
check 1 :: 2 :: nil
check 1 :: 2 :: 3 :: 4 :: 5 :: nil

3
tests/lean/notation2.lean.expected.out Normal file
View file

@ -0,0 +1,3 @@
notation2.lean:2:0: warning: imported file uses 'sorry'
1 :: 2 :: nil : list num
1 :: 2 :: 3 :: 4 :: 5 :: nil : list num