Да, используйте тактику idtac.
Вы можете передать idtac константную строку для печати.Он также может печатать идентификаторы (например, имена гипотез), если вы сопоставляете их с шаблоном, и может печатать их типы, если вы получаете доступ к ним с сопоставлением с шаблоном или type of.Вы также можете распечатать термины или содержимое переменных Ltac let-bound.Наконец, вы можете передать 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.