From bbc70c4cf0418a8ed5bc80bc32033f9f31c88fe5 Mon Sep 17 00:00:00 2001
From: Yuri de Wit <ydewit@gmail.com>
Date: Wed, 14 Sep 2022 18:44:41 -0300
Subject: [PATCH] fix: fixes #1599 by adding correct indentation

---
 src/Lean/Elab/Deriving/Repr.lean          | 8 +++-----
 tests/lean/derivingRepr.lean.expected.out | 2 +-
 2 files changed, 4 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean
index c14736f007..2b5289bd96 100644
--- a/src/Lean/Elab/Deriving/Repr.lean
+++ b/src/Lean/Elab/Deriving/Repr.lean
@@ -26,21 +26,19 @@ def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM Term :
   let target     := mkIdent header.targetNames[0]!
   forallTelescopeReducing ctorVal.type fun xs _ => do
     let mut fields ← `(Format.nil)
-    let mut first := true
     if xs.size != numParams + fieldNames.size then
       throwError "'deriving Repr' failed, unexpected number of fields in structure"
     for i in [:fieldNames.size] do
       let fieldName := fieldNames[i]!
       let fieldNameLit := Syntax.mkStrLit (toString fieldName)
       let x := xs[numParams + i]!
-      if first then
-        first := false
-      else
+      if i > numParams then
         fields ← `($fields ++ "," ++ Format.line)
       if (← isType x <||> isProof x) then
         fields ← `($fields ++ $fieldNameLit ++ " := " ++ "_")
       else
-        fields ← `($fields ++ $fieldNameLit ++ " := " ++ repr ($target.$(mkIdent fieldName):ident))
+        let indent := Syntax.mkNumLit <| toString ((toString fieldName |>.length) + " := ".length)
+        fields ← `($fields ++ $fieldNameLit ++ " := " ++ (Format.group (Format.nest $indent (repr ($target.$(mkIdent fieldName):ident)))))
     `(Format.bracket "{ " $fields:term " }")
 
 def mkBodyForInduct (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Term := do
diff --git a/tests/lean/derivingRepr.lean.expected.out b/tests/lean/derivingRepr.lean.expected.out
index bda7127782..f5bdbc2429 100644
--- a/tests/lean/derivingRepr.lean.expected.out
+++ b/tests/lean/derivingRepr.lean.expected.out
@@ -1,6 +1,6 @@
 { name := "Joe",
   val := [40, 39, 38, 37, 36, 35, 34, 33, 32, 31, 30, 29, 28, 27, 26, 25, 24, 23, 22, 21, 20, 19, 18, 17, 16, 15, 14,
-   13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1],
+          13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1],
   lower := 40,
   inv := _,
   flag := true }