有没有办法在 Ltac 过程中打印变量的值(无论是假设、策略还是术语)？
最佳答案
是的，使用 idtac战术。
您可以通过idtac要打印的常量字符串。如果您进行模式匹配，它还可以打印标识符(如假设名称)；如果您通过模式匹配或 type of 访问它们，它可以打印它们的类型。 。您还可以打印 Ltac let 绑定(bind)变量的术语或内容。最后可以通过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.
关于coq - Ltac 中可能出现 "printf-debugging"吗？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/52997319/