feat: check if "has already been declared" at the beginning

src/Init/Lean/Elab/DeclModifiers.lean

@@ -116,6 +116,11 @@ match modifiers.visibility with
   pure declName
 | _                  => pure declName
 
+def checkNotAlreadyDeclared (ref : Syntax) (declName : Name) : CommandElabM Unit := do
+env ← getEnv;
+when (env.contains declName) $
+  throwError ref ("'" ++ declName ++ "' has already been declared")
+
 def applyAttributes (ref : Syntax) (declName : Name) (attrs : Array Attribute) (applicationTime : AttributeApplicationTime) : CommandElabM Unit :=
 attrs.forM $ fun attr => do
  env ← getEnv;

src/Init/Lean/Elab/Definition.lean

@@ -145,6 +145,7 @@ def elabDefLike (view : DefView) : CommandElabM Unit :=
 let ref := view.ref;
 withDeclId view.declId $ fun name => do
   declName          ← mkDeclName view.modifiers name;
+  checkNotAlreadyDeclared ref declName;
   applyAttributes ref declName view.modifiers.attrs AttributeApplicationTime.beforeElaboration;
   explictLevelNames ← getLevelNames;
   decl? ← runTermElabM declName $ fun vars => Term.elabBinders view.binders.getArgs $ fun xs =>