From ab047cc4d1b970dff0ebae9968683f25eef0b392 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 19 Oct 2020 12:06:59 -0700
Subject: [PATCH] chore: remove unnecessary file

---
 src/Lean/Elab/Exception.lean |  2 +-
 src/Lean/Meta/Basic.lean     |  7 ++++++-
 src/Lean/Meta/Exception.lean | 23 -----------------------
 3 files changed, 7 insertions(+), 25 deletions(-)
 delete mode 100644 src/Lean/Meta/Exception.lean

diff --git a/src/Lean/Elab/Exception.lean b/src/Lean/Elab/Exception.lean
index 7775c769e8..c83821eee7 100644
--- a/src/Lean/Elab/Exception.lean
+++ b/src/Lean/Elab/Exception.lean
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.InternalExceptionId
-import Lean.Meta.Exception
+import Lean.Meta.Basic
 
 namespace Lean.Elab
 initialize postponeExceptionId : InternalExceptionId ← registerInternalExceptionId `postpone
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 024636754a..9a307b34ab 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -11,7 +11,6 @@ import Lean.Util.Trace
 import Lean.Util.RecDepth
 import Lean.Util.PPExt
 import Lean.Compiler.InlineAttrs
-import Lean.Meta.Exception
 import Lean.Meta.TransparencyMode
 import Lean.Meta.DiscrTreeTypes
 import Lean.Eval
@@ -30,6 +29,12 @@ They are packed into the MetaM monad.
 namespace Lean
 namespace Meta
 
+def registerIsDefEqStuckId : IO InternalExceptionId :=
+registerInternalExceptionId `isDefEqStuck
+
+@[init registerIsDefEqStuckId]
+constant isDefEqStuckExceptionId : InternalExceptionId := arbitrary _
+
 structure Config :=
 (foApprox           : Bool := false)
 (ctxApprox          : Bool := false)
diff --git a/src/Lean/Meta/Exception.lean b/src/Lean/Meta/Exception.lean
deleted file mode 100644
index bc1d142a7d..0000000000
--- a/src/Lean/Meta/Exception.lean
+++ /dev/null
@@ -1,23 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-import Lean.Environment
-import Lean.MetavarContext
-import Lean.Message
-import Lean.CoreM
-import Lean.InternalExceptionId
-import Lean.Util.PPGoal
-
-namespace Lean
-namespace Meta
-
-def registerIsDefEqStuckId : IO InternalExceptionId :=
-registerInternalExceptionId `isDefEqStuck
-
-@[init registerIsDefEqStuckId]
-constant isDefEqStuckExceptionId : InternalExceptionId := arbitrary _
-
-end Meta
-end Lean