Catch all exceptions

Stream: metaprogramming / tactics

[Leni Aniva]

Is there a way to catch all exceptions including internal exceptions, when running a CoreM monad?

e.g.

try
    Lean.tryCatchRuntimeEx (
      withReader ({ · with cancelTk? := .some cancelTk }) do
      Core.withCurrHeartbeats metaM.run') λ _e => pure false
catch e =>
  ...

This doesn't catch internal exception #0.

[Sebastian Ullrich]

let _ := MonadAlwaysExcept.except (m := CoreM)
try
  ...