how to determine the type of an exception?

Stream: lean4

[Scott Morrison]

Say I want to catch typeclass synthesis exceptions, but not others. What is the preferred way to do this? I have:

(← e.toMessageData.toString).startsWith "failed to synthesize"

[Eric Wieser]

I found myself wanting to do this too

[Eric Wieser]

In lean3 we're pretty bad at just blindly catching everything, which makes it hard to debug tactics by throwing errors when things go wrong

[Scott Morrison]

Okay, perhaps for now I will add an Exception.isFailedToSynthesize with this implementation so it can be used elsewhere, and we can come up with a better implementation later?

[Scott Morrison]

Okay, I've pushed this to !4#2611.