chore: cleanup (#4494)

closes #4287 closes #4288
leanprover · Jun 18, 2024 · 294b1d5 · 294b1d5
1 parent 1677719
commit 294b1d5
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 4 deletions.
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
@@ -2976,7 +2976,7 @@ def MonadExcept.ofExcept [Monad m] [MonadExcept ε m] : Except ε α → m α
 
 export MonadExcept (throw tryCatch ofExcept)
 
-instance (ε : outParam (Type u)) (m : Type v → Type w) [MonadExceptOf ε m] : MonadExcept ε m where
+instance (ε : Type u) (m : Type v → Type w) [MonadExceptOf ε m] : MonadExcept ε m where
   throw    := throwThe ε
   tryCatch := tryCatchThe ε
 

diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
@@ -194,9 +194,6 @@ def checkSystem : SynthM Unit := do
   Core.checkInterrupted
   Core.checkMaxHeartbeatsCore "typeclass" `synthInstance.maxHeartbeats (← read).maxHeartbeats
 
-@[inline] def mapMetaM (f : forall {α}, MetaM α → MetaM α) {α} : SynthM α → SynthM α :=
-  monadMap @f
-
 instance : Inhabited (SynthM α) where
   default := fun _ _ => default