小编Kev*_*len的帖子

在尝试创建循环遍历可变长度参数列表的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." *)