fix: fix deriving Repr for structure-like inductives

The deriving code currently uses isStructureLike when choosing whether to use
Inductive or Structure logic, which fails for inductives that are
structure-like. The commit changes the code to use isStructure.

src/Lean/Elab/Deriving/Repr.lean

@@ -78,7 +78,7 @@ where
     return alts
 
 def mkBody (ctx : Context) (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Syntax := do
-  if isStructureLike (← getEnv) indVal.name then
+  if isStructure (← getEnv) indVal.name then
     mkBodyForStruct ctx header indVal
   else
     mkBodyForInduct ctx header indVal auxFunName

tests/lean/derivingRepr.lean

@@ -15,6 +15,12 @@ inductive Tree (α : Type) where
 
 #eval Tree.node (List.iota 10 |>.map fun i => Tree.node [Tree.leaf i] (i%2==0)) true
 
+inductive StructureLikeInductive where
+  | field : Nat -> StructureLikeInductive
+  deriving Repr
+
+#eval StructureLikeInductive.field 5
+
 namespace Foo
 mutual
 inductive Tree (α : Type u) where

tests/lean/derivingRepr.lean.expected.out

@@ -16,6 +16,7 @@ Tree.node
    Tree.node [Tree.leaf 2] true,
    Tree.node [Tree.leaf 1] false]
   true
+StructureLikeInductive.field 5
 Foo.Tree.node
   (Foo.TreeList.cons
     (Foo.Tree.leaf 30)