diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index e58e6672c0..9d37683985 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -27,8 +27,6 @@ def checkValidInductiveModifier [Monad m] [MonadError m] (modifiers : Modifiers) throwError "invalid use of 'noncomputable' in inductive declaration" if modifiers.isPartial then throwError "invalid use of 'partial' in inductive declaration" - unless modifiers.attrs.size == 0 || (modifiers.attrs.size == 1 && modifiers.attrs[0].name == `class) do - throwError "invalid use of attributes in inductive declaration" def checkValidCtorModifier [Monad m] [MonadError m] (modifiers : Modifiers) : m Unit := do if modifiers.isNoncomputable then diff --git a/tests/lean/inductive1.lean b/tests/lean/inductive1.lean index b16f61ee6d..f9d638bbe4 100644 --- a/tests/lean/inductive1.lean +++ b/tests/lean/inductive1.lean @@ -79,7 +79,7 @@ end Boo partial inductive T1 : Type -- invalid use of partial noncomputable inductive T1 : Type -- invalid use of noncomputable -@[inline] inductive T1 : Type -- invalid use of attributes +@[inline] inductive T1' : Type -- declaration is not a definition private inductive T1 : Type | private mk : T1 -- invalid private constructor in private inductive type diff --git a/tests/lean/inductive1.lean.expected.out b/tests/lean/inductive1.lean.expected.out index 9587a443b0..82dfbce113 100644 --- a/tests/lean/inductive1.lean.expected.out +++ b/tests/lean/inductive1.lean.expected.out @@ -18,7 +18,7 @@ inductive1.lean:69:2-69:5: error: 'Boo.T1.bla' has already been declared inductive1.lean:73:10-73:12: error: 'Boo.T1' has already been declared inductive1.lean:80:0-80:27: error: invalid use of 'partial' in inductive declaration inductive1.lean:81:0-81:33: error: invalid use of 'noncomputable' in inductive declaration -inductive1.lean:82:0-82:29: error: invalid use of attributes in inductive declaration +inductive1.lean:82:10-82:30: error: declaration is not a definition 'T1'' inductive1.lean:85:0-85:17: error: invalid 'private' constructor in a 'private' inductive datatype inductive1.lean:93:7-93:26: error: invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes inductive1.lean:100:0-100:4: error: constructor resulting type must be specified in inductive family declaration