max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: inductive command

Browse source
This commit is contained in:
Leonardo de Moura 2020-07-13 13:31:36 -07:00
parent 3fc6d8ce61
commit 77ad630c80
2 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
tests/lean/inductive1.lean
View file

@ -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

3
tests/lean/inductive1.lean.expected.out
View file

@ -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