From a703610347672d0545f061a28e481cb33b4bbc3a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 21 Jul 2020 15:12:12 -0700
Subject: [PATCH] chore: reject `private` fields for now

See comment at `src/Lean/Structure.lean`
---
 src/Lean/Elab/Structure.lean | 2 ++
 1 file changed, 2 insertions(+)

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 ()
 
 /-