show_term { tac } runs the tactic tac,
and then prints the term that was constructed.
This is useful for
- constructing term mode proofs from tactic mode proofs, and
- understanding what tactics are doing, and how metavariables are handled.
As an example, in
example {P Q R : Prop} (h₁ : Q → P) (h₂ : R) (h₃ : R → Q) : P ∧ R :=
by show_term { tauto }
the term mode proof ⟨h₁ (h₃ h₂), eq.mpr rfl h₂⟩ produced by tauto will be printed.
As another example, if the goal is ℕ × ℕ, show_term { split, exact 0 } will
print refine (0, _), and afterwards there will be one remaining goal (of type ℕ).
This indicates that split, exact 0 partially filled in the original metavariable,
but created a new metavariable for the resulting sub-goal.