fix: do not display implicit fields

src/Lean/Elab/Deriving/Repr.lean

@@ -68,10 +68,12 @@ where
           let x := xs[indVal.numParams + i]
           let a := mkIdent (← mkFreshUserName `a)
           ctorArgs := ctorArgs.push a
-          if (← inferType x).isAppOf indVal.name then
-            rhs ← `($rhs ++ Format.line ++ $(mkIdent auxFunName):ident $a:ident max_prec)
-          else
-            rhs ← `($rhs ++ Format.line ++ reprArg $a)
+          let localDecl ← getLocalDecl x.fvarId!
+          if localDecl.binderInfo.isExplicit then
+            if (← inferType x).isAppOf indVal.name then
+              rhs ← `($rhs ++ Format.line ++ $(mkIdent auxFunName):ident $a:ident max_prec)
+            else
+              rhs ← `($rhs ++ Format.line ++ reprArg $a)
         patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs:term*))
         `(matchAltExpr| | $[$patterns:term],* => Repr.addAppParen (Format.group (Format.nest (if prec >= max_prec then 1 else 2) ($rhs:term))) prec)
       alts := alts.push alt

tests/lean/tabulate.lean

@@ -0,0 +1,13 @@
+inductive Vector (α : Type u) : Nat → Type u
+  | nil : Vector α 0
+  | cons : α → Vector α n → Vector α (n+1)
+  deriving Repr
+
+infix:67 " :: " => Vector.cons
+
+def tabulate (f : Fin n → α) : Vector α n :=
+  match n with
+  | 0   => Vector.nil
+  | n+1 => f 0 :: tabulate (f ∘ Fin.succ)
+
+#eval tabulate fun i : Fin 5 => i

tests/lean/tabulate.lean.expected.out

@@ -0,0 +1 @@
+Vector.cons 0 (Vector.cons 1 (Vector.cons 2 (Vector.cons 3 (Vector.cons 4 (Vector.nil)))))