Trace tauto，完成

Question

有没有办法在精益中追踪

tauto

、

finish

策略（或其他不属于 simp 的策略）？ 例如

example (P Q : Prop) : a → b ↔ ¬a ∨ b := by tauto

我希望看到应用于术语的必要重写或定理以证明目标，以便在更复杂的情况下明确使用它们。

Answer 1

import tactic

theorem foo (a b : Prop) : a → b ↔ ¬a ∨ b := by tauto!

#print foo

向您显示该策略创建的术语。但是强大的策略并不是为了产生可读的术语而设计的，所以你的里程可能会有所不同。