Better deprecation warnings

Stream: general

[Ruben Van de Velde]

I just came across this:

`div_add_div_same` has been deprecated: Use `add_div` instead

Note: The updated constant has a different type:
  ∀ {K : Type u_1} [inst : DivisionSemiring K] (a b c : K), (a + b) / c = a / c + b / c
instead of
  ∀ {K : Type u_1} [inst : DivisionSemiring K] (a b c : K), a / c + b / c = (a + b) / c

and wanted to thank whoever is responsible for that feature!

[Riccardo Brasca]

Is this written by hand or is there some automation?

[Markus Himmel]

lean4#9606 by Joseph Rotella

[Aaron Liu]

I'm a bit worried about the universe parameters

[Aaron Liu]

yeah it uses the universe parameter names instead of their positions

[Bhavik Mehta]

@Jason Reed I think this explains the message you mentioned to me last week:

Note: The updated constant has a different type:
  Type u → outParam (Type v) → Type (max u v)
instead of
  Type u_1 → outParam (Type u_2) → Type (max u_1 u_2)

(Do we not compare universe expressions up to $\alpha$-equivalence?)

[Jason Reed]

Huh, interesting, it sure does!