feat: throw error at field names starting with '_'

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 {

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)