From 596a3af1a02f4bc45a24831f63f3ac2a9bf22d13 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 9 Apr 2020 15:29:10 -0700
Subject: [PATCH] feat: check if "has already been declared" at the beginning

---
 src/Init/Lean/Elab/DeclModifiers.lean | 5 +++++
 src/Init/Lean/Elab/Definition.lean    | 1 +
 2 files changed, 6 insertions(+)

diff --git a/src/Init/Lean/Elab/DeclModifiers.lean b/src/Init/Lean/Elab/DeclModifiers.lean
index 6c102acb79..525e413394 100644
--- a/src/Init/Lean/Elab/DeclModifiers.lean
+++ b/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;
diff --git a/src/Init/Lean/Elab/Definition.lean b/src/Init/Lean/Elab/Definition.lean
index d99c6504d0..eeeccdf36a 100644
--- a/src/Init/Lean/Elab/Definition.lean
+++ b/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 =>