agda layer #

The agda layer enables support for the Agda proof assistant/programming language. This is achieved by using the official Agda Language Server and the Cornelis plugin (i.e., agda-mode aka Emacs mode, but for Neovim). The latter requires stack.

Bindings #

Some default bindings are provided for Cornelis. They are the same as the ones specified in Cornelis’s example configuration. In normal mode:

• <leader>l loads and type-checks the buffer;
• <leader>r refines the goal;
• <leader>d performs a case distinction/split;
• <leader>, shows goal type and context;
• <leader>. shows inferred type of hole contents;
• <leader>n solves constraints;
• <leader>a performs an automatic proof search;
• gd goes to definition;
• [/ jumps to previous goal;
• /] jumps to next goal;
• <C-A> is like agda-mode’s <C-A>, but also targets sub/super-scripts;
• <C-X> is like agda-mode’s <C-X>, but also targets sub/super-scripts.

Configuration #

Any vim global variable mentioned in the “Configuration” section of Cornelis is also a valid field for this layer’s config, as long as you strip the cornelis_ prefix.

Examples #

-- path/of/your/vim/config/init.lua

require("visimp")({
  agda = {
    max_size = 30 -- do not use the cornelis_ prefix for Cornelis settings
    lspconfig = {
      -- your Agda Language Server config
    }
  },
  languages = {
    "agda"
  }
})

Documentation #

• language server;
• Cornelis.