max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: MonadAlwaysExcept for MonadCacheT (#3726)

Browse source
This commit is contained in:
Sebastian Ullrich 2024-03-21 10:01:13 +01:00 • committed by GitHub
parent 2c15cdda04
commit 4d4e467392
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 9 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Lean/Util/Trace.lean
View file

@ -189,18 +189,22 @@ really need to handle (and then re-throw) every exception lest we end up with a
class MonadAlwaysExcept (ε : outParam (Type u)) (m : Type u → Type v) where
except : MonadExceptOf ε m
-- instance sufficient for inferring `MonadAlwaysExcept` for the elaboration monads
-- instances sufficient for inferring `MonadAlwaysExcept` for the elaboration monads
instance (ε) : MonadAlwaysExcept ε (EIO ε) where
instance : MonadAlwaysExcept ε (EIO ε) where
except := inferInstance
instance (ε) [always : MonadAlwaysExcept ε m] : MonadAlwaysExcept ε (StateT σ m) where
instance [always : MonadAlwaysExcept ε m] : MonadAlwaysExcept ε (StateT σ m) where
except := let _ := always.except; inferInstance
instance (ε) [always : MonadAlwaysExcept ε m] : MonadAlwaysExcept ε (StateRefT' ω σ m) where
instance [always : MonadAlwaysExcept ε m] : MonadAlwaysExcept ε (StateRefT' ω σ m) where
except := let _ := always.except; inferInstance
instance (ε) [always : MonadAlwaysExcept ε m] : MonadAlwaysExcept ε (ReaderT ρ m) where
instance [always : MonadAlwaysExcept ε m] : MonadAlwaysExcept ε (ReaderT ρ m) where
except := let _ := always.except; inferInstance
instance [always : MonadAlwaysExcept ε m] [STWorld ω m] [BEq α] [Hashable α] :
MonadAlwaysExcept ε (MonadCacheT α β m) where
except := let _ := always.except; inferInstance
def withTraceNode [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] (cls : Name)