Coq:在变量参数列表上的Ltac定义? [英] Coq: Ltac definitions over variable argument lists?
本文介绍了Coq:在变量参数列表上的Ltac定义?的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!
问题描述
在尝试创建循环遍历可变长度参数列表的Ltac定义时,我在Coq 8.4pl2上遇到以下意外行为.有人可以向我解释吗?
While trying to create an Ltac definition that loops over a variable-length argument list, I encountered the following unexpected behavior on Coq 8.4pl2. Can anyone explain it to me?
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
的最后一次调用以查看发生了什么:
Let's expand the last invocation of ltac_loop
to see what's happening:
ltac_loop 1 1 0
-> (fun Y => idtac "hello"; ltac_loop Y) 1 0
-> (idtac "hello"; ltac_loop 1) 0
您可以看到问题所在:您试图将不是函数的内容应用于自变量,这会导致您看到错误.解决方案是以连续传递方式重写策略:
There you can see the problem: you are trying to apply something that is not a function to an argument, which results in the error you saw. The solution is to rewrite the tactic in continuation-passing style:
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.
这篇关于Coq:在变量参数列表上的Ltac定义?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!
查看全文