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

fix(frontends/lean/pp): bug when pretty printing kernel projections

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-27 17:09:02 -07:00
parent bd97f67f28
commit c746783c0d
1 changed files with 1 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

@ -1140,7 +1140,7 @@ auto pretty_fn::pp_mdata(expr const & e) -> result {
auto pretty_fn::pp_proj(expr const & e) -> result {
format arg_fmt = pp_child(proj_expr(e), max_bp()).fmt();
format idx_fmt(proj_idx(e).get_small_value());
format idx_fmt(proj_idx(e).get_small_value() + 1);
return result(arg_fmt + format(".") + idx_fmt);
}