fix: pp projection indices starting at 1

leanprover · Oct 15, 2023 · c0b021e · c0b021e
1 parent 3e79ddd
commit c0b021e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/library/print.cpp b/src/library/print.cpp
@@ -246,7 +246,7 @@ struct print_expr_fn {
             break;
         case expr_kind::Proj:
             print_child(proj_expr(a));
-            out() << "." << proj_idx(a).to_mpz();
+            out() << "." << proj_idx(a).to_mpz() + 1;
             break;
         case expr_kind::BVar:
             out() << "#" << bvar_idx(a);