juvix-mode: Would be nice to have a choice on where to jump

[mariari]

In my tak benchmark, I have to layout the file like

terminating tak      : ℕ → ℕ → ℕ → ℕ;
terminating tak-then : ℕ → ℕ → ℕ → Unit -> ℕ;
            tak-else : ℕ → Unit → ℕ;

tak-then x y z unit ≔
  (tak (tak (-① x) y z)
       (tak (-① y) z x)
       (tak (-① z) x y));

tak-else z unit ≔ z;

tak x y z ≔
  if (isLT (compare y x))
     (box (tak-then x y z))
     (box (tak-else z));

when I Meta point on tak-else, it jumps to the type definition, however this can be quite far from the defn if I use a lot of mutually recursive functions.

Would be cool if I get a menu like

https://pomf2.lain.la/f/hadaxg65.png
https://pomf2.lain.la/f/4zqn99nj.png

It makes Meta point a bit tedious (having to go through the menu), but makes it nice to jump to the type spec or the implementation