From 96b49261e62ee99ac6372912f018bdce148bc80d Mon Sep 17 00:00:00 2001
From: pcpthm <pcpthm@gmail.com>
Date: Sat, 1 Oct 2022 10:01:31 +0900
Subject: [PATCH] fix: derive Repr missing a comma

---
 src/Lean/Elab/Deriving/Repr.lean  |  2 +-
 tests/lean/1668.lean              | 18 ++++++++++++++++++
 tests/lean/1668.lean.expected.out |  2 ++
 3 files changed, 21 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/1668.lean
 create mode 100644 tests/lean/1668.lean.expected.out

diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean
index 2b5289bd96..d7638f551a 100644
--- a/src/Lean/Elab/Deriving/Repr.lean
+++ b/src/Lean/Elab/Deriving/Repr.lean
@@ -32,7 +32,7 @@ def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM Term :
       let fieldName := fieldNames[i]!
       let fieldNameLit := Syntax.mkStrLit (toString fieldName)
       let x := xs[numParams + i]!
-      if i > numParams then
+      if i != 0 then
         fields ← `($fields ++ "," ++ Format.line)
       if (← isType x <||> isProof x) then
         fields ← `($fields ++ $fieldNameLit ++ " := " ++ "_")
diff --git a/tests/lean/1668.lean b/tests/lean/1668.lean
new file mode 100644
index 0000000000..c70a0ffb7f
--- /dev/null
+++ b/tests/lean/1668.lean
@@ -0,0 +1,18 @@
+structure Point where
+  x : Nat
+  y : Nat
+deriving Repr
+
+structure PPoint (α : Type) where
+  x : α
+  y : α
+deriving Repr
+
+def origin : Point :=
+  { x := Nat.zero, y := Nat.zero }
+
+def natOrigin : PPoint Nat :=
+  { x := Nat.zero, y := Nat.zero }
+
+#eval origin
+#eval natOrigin
diff --git a/tests/lean/1668.lean.expected.out b/tests/lean/1668.lean.expected.out
new file mode 100644
index 0000000000..1007552ba5
--- /dev/null
+++ b/tests/lean/1668.lean.expected.out
@@ -0,0 +1,2 @@
+{ x := 0, y := 0 }
+{ x := 0, y := 0 }