Code navigation

[ajirving]

It would be really helpful if some of the standard Emacs functions for navigating code worked in Lean4 mode. Is it possible to make beginning-of_defun (c-m-a), end-of-defun (c-m-e) move to the beginning/end of the current proof? Could backward-up-list (c-m-u) move to the start of the proof of the current subgoal? I know the Lean syntax is very complicated so doing this perfectly might be hard but even something based only on indentation would be helpful.

Do other users have any tips for navigating long proofs in Emacs without these commands? I use them all the time in other language modes.

[mekeor]

Thanks for reporting. I agree that Lean4-Mode should offer this kind of feature.

If you are impatient, you might use this repository by @ultronozm https://github.com/ultronozm/czm-lean4.el and their related repositories. Personally, I would not expect them to be stable for everyone but rather personal projects.