the rest

leanprover · Sep 10, 2024 · f3c344e · f3c344e
1 parent 7f1e1c6
commit f3c344e
Show file tree

Hide file tree

Showing 5 changed files with 5 additions and 5 deletions.
diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean
@@ -63,7 +63,7 @@ instance : MonadFunctor m (OptionT m) := ⟨fun f x => f x⟩
   let some a ← x | handle ()
   pure a
 
-instance : MonadExceptOf Unit (OptionT m) where
+instance (priority := low) : MonadExceptOf Unit (OptionT m) where
   throw    := fun _ => OptionT.fail
   tryCatch := OptionT.tryCatch
 

diff --git a/src/Init/Control/State.lean b/src/Init/Control/State.lean
@@ -113,7 +113,7 @@ def ForM.forIn [Monad m] [ForM (StateT β (ExceptT β m)) ρ α]
 section
 variable {σ : Type u} {m : Type u → Type v}
 
-instance [Monad m] : MonadStateOf σ (StateT σ m) where
+instance (priority := high) [Monad m] : MonadStateOf σ (StateT σ m) where
   get       := StateT.get
   set       := StateT.set
   modifyGet := StateT.modifyGet

diff --git a/src/lake/Lake/Util/Cycle.lean b/src/lake/Lake/Util/Cycle.lean
@@ -62,7 +62,7 @@ instance (priority := high) [Monad m] : MonadCallStackOf κ (CallStackT κ m) wh
 /-- A transformer that equips a monad with a `CallStack` to detect cycles. -/
 abbrev CycleT κ m := CallStackT κ <| ExceptT (Cycle κ) m
 
-instance [Monad m] : MonadCycleOf κ (CycleT κ m) where
+instance (priority := high) [Monad m] : MonadCycleOf κ (CycleT κ m) where
   throwCycle := throw
 
 /--

diff --git a/src/lake/Lake/Util/EStateT.lean b/src/lake/Lake/Util/EStateT.lean
@@ -183,7 +183,7 @@ protected def get [Pure m] : EStateT ε σ m σ := fun s =>
 protected def modifyGet [Pure m] (f : σ → Prod α σ) : EStateT ε σ m α := fun s =>
   match f s with | (a, s) => pure <| .ok a s
 
-instance [Pure m] : MonadStateOf σ (EStateT ε σ m) where
+instance (priority := high) [Pure m] : MonadStateOf σ (EStateT ε σ m) where
   set       := EStateT.set
   get       := EStateT.get
   modifyGet := EStateT.modifyGet

diff --git a/src/lake/Lake/Util/Store.lean b/src/lake/Lake/Util/Store.lean
@@ -28,7 +28,7 @@ class MonadDStore (κ : Type u) (β : semiOutParam $ κ → Type v) (m : Type v
   fetch? : (key : κ) → m (Option (β key))
   store : (key : κ) → β key → m PUnit
 
-instance [MonadDStore κ β m] : MonadStore1Of k (β k) m where
+instance (priority := high) [MonadDStore κ β m] : MonadStore1Of k (β k) m where
   fetch? := MonadDStore.fetch? k
   store o := MonadDStore.store k o