如何同时看待多个目标？

Question

我正在考虑编写策略，该策略将考虑多个目标并据此做出决策。但是，当我match goal with盯着一个目标使用时，怎么说“请找到另一个看起来像这样的目标”？

---

或更确切地说，一个更笼统的问题是，如何在Ltac中切换目标？

Answer 1

正如我们在评论中讨论的那样，在 Ltac 中目前不可能实现对当前证明目标的这种检查。

然而，可以在 ocaml 级别或使用一种较新的策略语言（如ltac2或 ）对这样的策略进行编程mtac。