From de2df5955f110bf4bdbdf4d4b014b6b3b0b83e00 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 26 Aug 2020 13:42:57 -0700
Subject: [PATCH] refactor: polymorphic checkNotAlreadyDeclared

---
 src/Lean/Elab/DeclModifiers.lean | 29 +++++++++++++++--------------
 1 file changed, 15 insertions(+), 14 deletions(-)

diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean
index 1ef377c9b8..537a225a66 100644
--- a/src/Lean/Elab/DeclModifiers.lean
+++ b/src/Lean/Elab/DeclModifiers.lean
@@ -8,6 +8,21 @@ import Lean.Elab.Attributes
 
 namespace Lean
 namespace Elab
+
+def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] (declName : Name) : m Unit := do
+env ← getEnv;
+when (env.contains declName) $
+  match privateToUserName? declName with
+  | none          => throwError ("'" ++ declName ++ "' has already been declared")
+  | some declName => throwError ("private declaration '" ++ declName ++ "' has already been declared");
+when (env.contains (mkPrivateName env declName)) $
+  throwError ("a private declaration '" ++ declName ++ "' has already been declared");
+match privateToUserName? declName with
+| none => pure ()
+| some declName =>
+  when (env.contains declName) $
+    throwError ("a non-private declaration '" ++ declName ++ "' has already been declared")
+
 namespace Command
 
 inductive Visibility
@@ -87,20 +102,6 @@ pure {
   attrs           := attrs
 }
 
-def checkNotAlreadyDeclared (declName : Name) : CommandElabM Unit := do
-env ← getEnv;
-when (env.contains declName) $
-  match privateToUserName? declName with
-  | none          => throwError ("'" ++ declName ++ "' has already been declared")
-  | some declName => throwError ("private declaration '" ++ declName ++ "' has already been declared");
-when (env.contains (mkPrivateName env declName)) $
-  throwError ("a private declaration '" ++ declName ++ "' has already been declared");
-match privateToUserName? declName with
-| none => pure ()
-| some declName =>
-  when (env.contains declName) $
-    throwError ("a non-private declaration '" ++ declName ++ "' has already been declared")
-
 def applyVisibility (visibility : Visibility) (declName : Name) : CommandElabM Name :=
 match visibility with
 | Visibility.private => do