假设我有一个像这样的策略（取自 HaysTac），它搜索一个参数来专门化一个特定的假设：
Ltac find_specialize_in H :=
multimatch goal with
| [ v : _ |- _ ] => specialize (H v)
end.
然而，我想写一个策略来搜索n专门化策略的参数。关键是还得回溯。例如，如果我有以下假设：
y : T
H : forall (x : T), x = y -> P x
x1 : T
x2 : T
Heq : x1 = y
如果我写do 2 (find_specialize_in H)，它可能会选择x2实例化它，然后尝试找到第二个参数失败。因此，我需要重复循环能够回溯它选择的参数来专门化较早的参数。
是否有可能做到这一点？我怎样才能制作一个策略循环来回溯之前迭代的选择？
None
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
