fstar-jump-to-definition on a module should jump to the fsti if it exists about fstar-mode.el HOT 1 OPEN

I think this is F* side; we just jump to the position it reports. But we could work around it on our side if needed. Here's I'd go about it (I don't have time to dive into it myself atm, but I think you could give it a try):

• Turn debugging on.
• Do a jump to definition
• Look at what F* returns; I don't recall if it's easily distinguishable from a usual jump to a specific definition (in fact, this might even be special-cased in fstar-mode to jump directly to a file)
• Find the corresponding bit in fstar-mode (ask me for help if this part is tricky)
• Change it to test if an fsti is present and jump there if so

I would predicate the last part on a setting, but I wouldn't object to making jumping to the fsti the default.

from fstar-mode.el.