在 Ltac 中实现复杂的策略时，有一些 Ltac 命令或策略调用我预计会失败以及预期失败(例如终止 repeat 或导致回溯)。这些故障通常在故障级别 0 时引发。
更高级别引发的故障“逃避”周围 try或 repeat阻止，并且可用于发出意外故障的信号。
我缺少的是一种运行策略的方法 tac并将其失败(即使是 0 级)视为更高级别，同时保留失败的消息。这会让我确保 repeat不会因我这边的 Ltac 编程错误而终止。
能不能在 Ltac 中实现这种提升失败级别的高阶战术？
最佳答案
您可以在 Ocaml 中编写策略来实现这一目标。我把它放在 GitHub here .
例如，以下应该引发错误而不是静默成功:
repeat (match goal with
| [ |- _ ] =>
raise_error_level (assert (3 = 3) by idtac)
end).
关于coq - 提高 coq 策略的失败级别，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/45109074/