From 49ebd30fd5c562eea453fe0ff628fad9e6034539 Mon Sep 17 00:00:00 2001 From: Zygimantas Straznickas Date: Mon, 22 Feb 2021 20:11:17 -0500 Subject: [PATCH] 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 | 2 +- tests/lean/derivingRepr.lean | 6 ++++++ tests/lean/derivingRepr.lean.expected.out | 1 + 3 files changed, 8 insertions(+), 1 deletion(-) 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)