Zulip Chat Archive

Stream: general

Topic: catching and displaying an exception in Lean 3


David Renshaw (Dec 21 2022 at 05:00):

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 (Dec 21 2022 at 08:08):

Is the code snippet in Lean 4?

David Renshaw (Dec 21 2022 at 12:24):

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

Alex J. Best (Dec 21 2022 at 12:35):

Perhaps docs#tactic.try_or_report_error

David Renshaw (Dec 21 2022 at 13:39):

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.


Last updated: Dec 20 2023 at 11:08 UTC