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

fix(frontends/lean/pp): let expressions

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-25 12:30:39 -07:00
parent c3c66b6c90
commit e765105ea5
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/pp.cpp
View file

@ -966,10 +966,10 @@ class pp_fn {
name const & n = std::get<0>(b); name const & n = std::get<0>(b);
format beg = i == 0 ? space() : line(); format beg = i == 0 ? space() : line();
format sep = i < sz - 1 ? comma() : format(); format sep = i < sz - 1 ? comma() : format();
result p_def = pp(std::get<2>(b), depth+1); result p_def = pp_scoped_child(std::get<2>(b), depth+1);
expr type = std::get<1>(b); expr type = std::get<1>(b);
if (type) { if (type) {
result p_type = pp(type, depth+1); result p_type = pp_scoped_child(type, depth+1);
r_format += nest(3 + 1, compose(beg, group(format{format(n), space(), r_format += nest(3 + 1, compose(beg, group(format{format(n), space(),
colon(), nest(n.size() + 1 + 1 + 1, compose(space(), p_type.first)), space(), g_assign_fmt, colon(), nest(n.size() + 1 + 1 + 1, compose(space(), p_type.first)), space(), g_assign_fmt,
nest(m_indent, format{line(), p_def.first, sep})}))); nest(m_indent, format{line(), p_def.first, sep})})));