From c746783c0d03eecb78878aa8ea956d7d8c2c4490 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 27 Sep 2018 17:09:02 -0700
Subject: [PATCH] fix(frontends/lean/pp): bug when pretty printing kernel
 projections

---
 src/frontends/lean/pp.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index e4207051eb..a34874ee08 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -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);
 }