"printf-debugging“在Ltac中是可能的吗？

Question

有没有办法在Ltac过程中间打印变量(无论是假设、策略还是术语)的值？

Answer 1

是的，使用idtac策略。

您可以向idtac传递一个要打印的常量字符串。如果您进行模式匹配，它还可以打印标识符(如假设名称)，如果您通过模式匹配或type of访问它们，它还可以打印它们的类型。您还可以打印术语或Ltac let绑定变量的内容。最后，您可以向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.