From 19fc369875fea86ea181f63c1e54bd0589333bf1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 21 Jul 2020 10:09:16 -0700
Subject: [PATCH] feat: throw error at field names starting with '_'

---
 src/Lean/Elab/Structure.lean | 2 ++
 tests/lean/struct1.lean      | 6 ++++++
 2 files changed, 8 insertions(+)

diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 08b1e8bfdf..6fcae75d80 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -129,6 +129,8 @@ fieldBinders.foldlM
     idents.foldlM
       (fun (views : Array StructFieldView) ident => do
         let name     := ident.getId;
+        when (isInternalSubobjectFieldName name) $
+          throwError ident ("invalid field name '" ++ name ++ "', identifiers starting with '_' are reserved to the system");
         let declName := structDeclName ++ name;
         declName ← applyVisibility ident modifiers.visibility declName;
         pure $ views.push {
diff --git a/tests/lean/struct1.lean b/tests/lean/struct1.lean
index c13aacafe8..280869c92b 100644
--- a/tests/lean/struct1.lean
+++ b/tests/lean/struct1.lean
@@ -17,3 +17,9 @@ structure S extends A Nat, A Bool := -- error field toA already declared
 
 structure S extends A Nat, B Bool := -- error field `x` from `B` has already been declared
 (x : Nat)
+
+structure S := -- error '_' is not allowed
+(_x : Nat)
+
+structure S := -- error '_' is not allowed
+(x _y : Nat)