提高coq战术的失败程度

Question

当在Ltac中实现复杂的策略时,有一些Ltac命令或策略调用我期望失败以及预期的位置(例如终止a repeat或导致回溯).这些故障通常在故障级别0时引发.

在较高级别上升的故障"逃离"周围try或repeat阻塞,并且对于发出意外故障是有用的.

我缺少的是一种运行策略tac并将其失败(即使在0级)处于更高水平,同时保留失败信息的方法.这将让我确保repeat不会因为我身边的Ltac编程错误而终止.

我能否在Ltac中实施这种提升级别的高阶战术？

Answer 1

您可以在 Ocaml 中编写策略来实现这一目标。我把它放在 GitHub上。

例如，以下内容应该引发错误，而不是默默地成功：

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