Michael Soegtrop (Mar 05 2021 at 11:18): 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?
Pierre-Marie Pédrot (Mar 05 2021 at 11:45):This refers to the backtracking mechanism, not the panic one.
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.
Pierre-Marie Pédrot (Mar 05 2021 at 11:47):There is no dedicated syntax for this, but you can roll your own notation.
Michael Soegtrop (Mar 05 2021 at 13:58):Thanks, I will try that!
Last updated: Apr 16 2024 at 19:01 UTC