From 77ad630c8007b3ee54ee46b653e4bdbe1d720d7e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 13 Jul 2020 13:31:36 -0700 Subject: [PATCH] test: inductive command --- tests/lean/inductive1.lean | 5 +++++ tests/lean/inductive1.lean.expected.out | 3 +++ 2 files changed, 8 insertions(+) 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