在尝试创建循环可变长度参数列表的 Ltac 定义时，我在 Coq 8.4pl2 上遇到了以下意外行为。谁能给我解释一下吗？
Ltac ltac_loop X :=
match X with
| 0 => idtac "done"
| _ => (fun Y => idtac "hello"; ltac_loop Y)
end.
Goal True.
ltac_loop 0. (* prints "done" as expected *)
ltac_loop 1 0. (* prints "hello" then "done" as expected *)
ltac_loop 1 1 0. (* unexpectedly yields "Error: Illegal tactic application." *)
让我们扩展最后一个调用ltac_loop看看发生了什么：
ltac_loop 1 1 0
-> (fun Y => idtac "hello"; ltac_loop Y) 1 0
-> (idtac "hello"; ltac_loop 1) 0
在那里您可以看到问题：您试图将不是函数的东西应用于参数，这会导致您看到的错误。解决方案是以连续传递的方式重写策略：
Ltac ltac_loop_aux k X :=
match X with
| 0 => k
| _ => (fun Y => ltac_loop_aux ltac:(idtac "hello"; k) Y)
end.
Ltac ltac_loop X := ltac_loop_aux ltac:(idtac "done") X.
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
