`generalize_proofs` #

A simple tactic to find and replace all occurrences of proof terms in the context and goal with new variables.

source

meta def tactic.generalize_proofs (ns : list name) (loc : interactive.loc) :

tactic unit

Generalize proofs in the goal, naming them with the provided list.

source

meta def tactic.interactive.generalize_proofs :

interactive.parse interactive.types.ident_* → interactive.parse interactive.types.location → tactic unit

Generalize proofs in the goal, naming them with the provided list.

For example:

example : list.nth_le [1, 2] 1 dec_trivial = 2 :=
begin
  -- ⊢ [1, 2].nth_le 1 _ = 2
  generalize_proofs h,
  -- h : 1 < [1, 2].length
  -- ⊢ [1, 2].nth_le 1 h = 2
end

generalize_proofs #

`generalize_proofs` #