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, ifexpr
not 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 {! !}
.