有没有办法在 Ltac 程序的中间打印变量的值（无论是假设、策略、术语）吗？
问问题
211 次
1 回答
2
是的，使用idtac策略。
您可以传递idtac一个常量字符串来打印。如果您对它们进行模式匹配，它还可以打印标识符（如假设名称），如果您通过模式匹配或type of. 您还可以打印术语或 Ltac 让绑定变量的内容。最后，您可以传递idtac多个参数以将它们全部打印出来。您提到了打印策略-不幸的是，这是您无法打印的一件事idtac。如果你尝试这样做，你只会得到<战术关闭>。
这里有一堆例子：
Goal True -> False.
intro Htrue.
idtac "hello world". (* prints hello world *)
match goal with
| [ H: True |- _ ] => idtac H (* prints Htrue *)
end.
match goal with
| |- ?g => idtac g (* prints False *)
end.
let t := type of Htrue in idtac t. (* prints True *)
let x := constr:(1 + 1) in idtac x. (* prints (1 + 1) *)
idtac "hello" "there". (* prints hello there *)
(* note that this is an Ltac-level function, not a Gallina function *)
let x := (fun _ => fail) in idtac x. (* prints <tactic closure> *)
Abort.
于 2018-10-26T02:00:25.143 回答