From 6a91fb16131d430c365dac9d4e05bc68eab8ee25 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 17 Sep 2020 13:50:43 +0200
Subject: [PATCH] fix: delaborating projections

---
 src/Lean/Delaborator.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean
index 02f6626502..3e5f20eca0 100644
--- a/src/Lean/Delaborator.lean
+++ b/src/Lean/Delaborator.lean
@@ -520,7 +520,8 @@ e ← withProj delab;
 -- not perfectly authentic: elaborates to the `idx`-th named projection
 -- function (e.g. `e.1` is `Prod.fst e`), which unfolds to the actual
 -- `proj`.
-`($(e).$(mkStxNumLitAux idx):fieldIdx)
+let idx := mkStxLit fieldIdxKind (toString (idx + 1));
+`($(e).$idx:fieldIdx)
 
 /-- Delaborate a call to a projection function such as `Prod.fst`. -/
 @[builtinDelab app]