Geek Answers Handbook

Increasing rejection rate in coq tactics

When implementing complex tactics in Ltac, there are some Ltac commands or tactical challenges that I expect to fail, and where this is expected (for example, to complete repeator to go back). These failures usually rise at failure level 0.

Failures raised at a higher level "exit" from the surrounding block tryor repeatare useful for reporting unexpected failures.

What I am missing is a way to start a tactic tacand handle its failure, even at level 0, at a higher level, saving the error message. This would allow me to make sure that it repeatdoes not end due to an Ltac programming error on my side.

Can I implement this higher order tactic at the failure level in Ltac?

+6
source share
2 answers

You can write tactics to achieve this goal in Ocaml. I put this on github here .

For example, the following should cause an error instead of the silent following:

repeat (match goal with 
          | [ |- _ ] => 
            raise_error_level (assert (3 = 3) by idtac)
        end).
+3
source

I don’t know if you can get exactly what you want, but I sometimes use the following idiom:

tactic_expression_that_may_fail_with_level_0
|| fail 1000 "There was some problem here"

If the first tactic fails with level 0, it ||will try to launch the second, which will fail at a very high level and will inform you about it.

, , , - .

+1

More articles:


All Articles