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

chore: reject private fields for now

Browse source 
See comment at `src/Lean/Structure.lean`
This commit is contained in:
Leonardo de Moura 2020-07-21 15:12:12 -07:00
parent 801acd3e62
commit a703610347
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -93,6 +93,8 @@ when modifiers.isUnsafe $
throwError ref "invalid use of 'unsafe' in field declaration";
when (modifiers.attrs.size != 0) $
throwError ref "invalid use of attributes in field declaration";
when modifiers.isPrivate $
throwError ref "private fields are not supported yet";
pure ()
/-