catching and displaying an exception in Lean 3

Stream: general

[David Renshaw]

In Lean 3 I can do try { ... } catch e => { ... }. Can I do something similar in Lean 3?

I'm detecting that an error is getting thrown on this line, but I don't know of a good way to examine what the error actually is.

[Martin Dvořák]

Is the code snippet in Lean 4?

[David Renshaw]

Oops, updated. Yes, the snippet is intended to be Lean 4. How do I do try ... catch in Lean 3?

[Alex J. Best]

Perhaps docs#tactic.try_or_report_error

[David Renshaw]

Thanks. The reported error indicated that I should do set_option trace.app_builder true. After doing that I no longer need to catch the error.