parent
167771923e
commit
294b1d5839
2 changed files with 1 additions and 4 deletions
|
|
@ -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 ε
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue