mathlib3 documentation

tactic.show_term

source
meta def tactic.interactive.show_term (t : tactic.interactive.itactic) :
tactic.interactive.itactic

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.

source
def tactic_doc.tactic.show_term  :
tactic_doc_entry

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.