feat: hover for cases/induction case names

[digama0]

This makes the zero and succ in

  induction x with
  | zero => ...
  | succ x => ...

into clickable links to the inductive constructors. It also does its best with custom inductives but most likely will not work unless the custom inductive is added manually. (Fundamentally this is because the case names correspond to local binding names in the recursor, not directly to definitions.)

[Vtec234]

It also does its best with custom inductives but most likely will not work unless the custom inductive is added manually.

Do you mean "with custom induction principles", or actually that Nat specifically somehow has special support?

[digama0]

I mean things that aren't inductives but try to act like one by having a bunch of theorems with names similar to the constructors and recursor of an inductive type. Because the implementation uses isInductive on the parent of the recursor, that means that if you have a Nat.myRecOn (where Nat could be any inductive) with minor premises named zero and succ, then the hovers will work, and will target Nat.zero and Nat.succ. If you name the minor premises foo and bar then nothing will be linked. And if you have MyNat.recOn where def MyNat := Nat, then even if MyNat.zero and MyNat.succ exist they will not be linked.