Simple agda integration with vim. It runs a single agda process for your vim session and communicates with it using pipes which are in vim-8.1. It is also using brand new popup windows which just landed in vim. So you'd likely need to compile vim from git.
The plugin includes:
- agda syntax script
- literate agda syntax script
- filetype plugin with the following commands and maps (check
ftplugin/agda.vim)::AgdaLoad- load current file, mapped to<LocalLeader>l:AgdaMetas- list goals:AgdaStart- start agda process (done automatically):AgdaStop- stop agda process:AgdaRestart- restart agda process:AgdaVersion- report version of agda:AgdaRefine- refine a value, mapped to<LocalLeader>r:AgdaAuto- solve current goal by using Auto, mapped to<LocalLeader>a:AgdaInfer [expr]- infer and normalise type of expression, ifexprnot given use current goal, mapped to<LocalLeader>t:AgdaAbort- abort last operation<LocalLeader>c- map which opens a popup with current goal context<LocalLeader>s- reads current keyword and reporpts where it comes from
It supports both {! !} and ? goals. Some commands, e.g. :AgdaAuto will
pass the inner part of {! !}.