diff --git a/tests/lean/inductive1.lean b/tests/lean/inductive1.lean
index 3d9cadfef6..19712eaa3d 100644
--- a/tests/lean/inductive1.lean
+++ b/tests/lean/inductive1.lean
@@ -76,3 +76,8 @@ inductive T1 : Type -- Boo.T1 has already been defined
 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
+
+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 c2c7d038a6..d8357f4794 100644
--- a/tests/lean/inductive1.lean.expected.out
+++ b/tests/lean/inductive1.lean.expected.out
@@ -17,3 +17,6 @@ inductive1.lean:59:0: error: invalid inductive type, universe parameters mismatc
 inductive1.lean:69:2: error: 'Boo.T1.bla' has already been declared
 inductive1.lean:73:10: error: 'Boo.T1' has already been declared
 inductive1.lean:78:8: error: invalid use of 'partial' in inductive declaration
+inductive1.lean:79:14: error: invalid use of 'noncomputable' in inductive declaration
+inductive1.lean:80:10: error: invalid use of attributes in inductive declaration
+inductive1.lean:83:0: error: invalid 'private' constructor in a 'private' inductive datatype