Open pnlph opened 4 years ago
Perhaps we can add a section for something like "Differences between Atom and Emacs mode"? And list the commands that currently only exist on one of the editors?
Yes, this is a good idea. Can you post here such a list and we upload a first version?
Hi,
i think it would be good to update the agda-mode/README.md here in the agda mode in order to specify which commands are shared with Emacs, which commands are only available here in Agda mode, and which commands are only on Emacs and pending integration with Atom.
I could edit the changes if we discuss them in this thread.
I had some doubts with the
go-to-definition
command and thought it was an Emacs one. See also agda/agda#4342