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

feat: allow attributes on structures and inductives

Browse source
This commit is contained in:
Gabriel Ebner 2021-12-23 15:19:26 +01:00 • committed by Leonardo de Moura
parent f43f74e78f
commit 70ef4e529c
3 changed files with 2 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Inductive.lean
View file

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

2
tests/lean/inductive1.lean
View file

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

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

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