3 ms·
It's really just basic editor support. Agda is quite an interactive programming language, so you need lots of shortcuts, syntax highlighting, autofilling etc in
by CHY872 11y ago
It's really just basic editor support. Agda is quite an interactive programming language, so you need lots of shortcuts, syntax highlighting, autofilling etc in order to get productivity at all (especially since you're constantly moving stuff in and out of a repl)
https://youtu.be/pP7ynVdVY9A?t=13m https://youtu.be/pP7ynVdVY9A?t=13m gives a decent example.
As to why support isn't in other editors, it's probably a combination of: more code to support, no one wants to write it, and the fact that Agda is less amenable to being sped up by efficient usage of editors (as it is a more interactive process with less copy pasting).
- black_knight 11y agoI have to disagree to that one needs syntax highlighting and autofilling to be productive in Agda. I have written a fair amount of agda code in Acme, which has neither. Rather I find these bells and whistles distracting — and prefer giving my complete attention to the task at hand. I think that writing agda code interactively in Emacs is fine, but it is certainly not the only way to write good agda code. In fact writing without the interactive support encourages better code structure. One is more likely to factor a complicated line into several help terms (using 'where', for example), which makes the code more readable.