coq - 什么都不做的战术是什么？

Question

有时采用什么都不做的策略很有用。我尝试搜索“empty tactic”或“null tactic”，但这些都没有给我答案。

Answer 1

您正在寻找的策略是idtac，“identity tactic”的缩写

 Tactic idtac (ident ​| string​ | natural)*

Leaves the proof unchanged and prints the given tokens. Strings and naturals are printed literally. If ident is an Ltac variable, its contents are printed; if not, it is an error. source

您可以提供 idtac 参数，这对调试很有用。