my workflow with agda lately has really been to use emacs as the "proof assistant" part (interactive development) and vim for everything else (reading/referencing files; opening things to show to others)
which makes me wonder if we shouldn't be thinking of "proof assistants" more as editor/dev tool support than as languages
...proof assistant server protocol? (maybe i'm reinventing proof general idk)
