mathlib3 documentation

tactic.show_term

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.

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.