diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 841c2e2ea7..7dc668d330 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -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 () /-