Stream: Ltac2

Topic: How to catch an exception


view this post on Zulip Michael Soegtrop (Mar 05 2021 at 11:18):

@Pierre-Marie Pédrot : the manual says at (https://coq.github.io/doc/master/refman/proof-engine/ltac2.html#exception-catching) that Ltac2 has proper exception catching. I wonder what the syntax is - the standard OCaml syntax doesn't work and looking at the .gml file also didn't enlighten me. Up to now I use a match! with an additional catch branch, but this doesn't allow me to catch only exceptions of a specific type. How would I do that?

view this post on Zulip Pierre-Marie Pédrot (Mar 05 2021 at 11:45):

This refers to the backtracking mechanism, not the panic one.

view this post on Zulip Pierre-Marie Pédrot (Mar 05 2021 at 11:46):

To catch an exception you can use Control.plus or Control.case, depending on the exact semantics you want.

view this post on Zulip Pierre-Marie Pédrot (Mar 05 2021 at 11:47):

There is no dedicated syntax for this, but you can roll your own notation.

view this post on Zulip Michael Soegtrop (Mar 05 2021 at 13:58):

Thanks, I will try that!


Last updated: Jan 31 2023 at 09:01 UTC