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

Fix bug when pretty printing function applications where the head is a meta-variable.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-03 17:51:56 -07:00
parent 51422fe654
commit 4a75e2d965
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/frontends/lean/lean_pp.cpp
View file

@ -648,8 +648,8 @@ class pp_fn {
} else { } else {
// standard function application // standard function application
expr const & f = app.get_function(); expr const & f = app.get_function();
result p = is_constant(f) ? mk_result(format(const_name(f)),1) : pp_child(f, depth); result p = is_constant(f) && !is_metavar(f) ? mk_result(format(const_name(f)),1) : pp_child(f, depth);
bool simple = is_constant(f) && const_name(f).size() <= m_indent + 4; bool simple = is_constant(f) && !is_metavar(f) && const_name(f).size() <= m_indent + 4;
unsigned indent = simple ? const_name(f).size()+1 : m_indent; unsigned indent = simple ? const_name(f).size()+1 : m_indent;
format r_format = p.first; format r_format = p.first;
unsigned r_weight = p.second; unsigned r_weight = p.second;