custom induction

Stream: general

[Kenny Lau]

Can we tag our induction lemmas and have the tactic induction recognize it? Maybe create a new tactic induction'?

[Chris Hughes]

You can do induction using

[Kenny Lau]

@Chris Hughes I can't work it out for polynomials

[Chris Hughes]

example (p : polynomial ℤ) : 1 = 2 :=
begin
  induction p using polynomial.induction_on,
end

[Kenny Lau]

can you put p in the result?

[Chris Hughes]

example (p : polynomial ℤ) : p = 2 :=
begin
  induction p using polynomial.induction_on,
end