diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean index 7309eaa1c8..3f2a3950ee 100644 --- a/src/Lean/Elab/Deriving/Repr.lean +++ b/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 diff --git a/tests/lean/derivingRepr.lean b/tests/lean/derivingRepr.lean index 597bfae37a..e88cc34f51 100644 --- a/tests/lean/derivingRepr.lean +++ b/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 diff --git a/tests/lean/derivingRepr.lean.expected.out b/tests/lean/derivingRepr.lean.expected.out index 418b11387c..bda7127782 100644 --- a/tests/lean/derivingRepr.lean.expected.out +++ b/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)