Skip to content

Latest commit

 

History

History
73 lines (58 loc) · 2.36 KB

README.md

File metadata and controls

73 lines (58 loc) · 2.36 KB
Raw

agda.nvim

NeoVim plugin for interacting with Agda written in Lua

(Note: Sorry for the lack of updates lately, currently I'm waiting for the following issue: agda/agda#5665 to be addressed, but in the meantime I might switch to the Lisp backend, which could be a bit painful in terms of parsing, but at least would enable the further development of this plugin.)

Dependencies

Installation

Plug

  Plug 'nvim-lua/plenary.nvim'
  Plug 'isti115/agda.nvim'

Usage

By default the usual agda actions are mapped to the conventional keys, preceded by <LocalLeader> (\ by default in NeoVim), such as:

  • \l - Load
  • \f - Next goal (Forward)
  • \c - Case split

and so on. See the source for all available actions!

Options

Option Possible Values (Defaults in bold)
g:agda_theme dark, light
g:agda_keymap vim, emacs, none

Features

Done*

  • Goal types
  • Version info
  • Case splitting
  • Context information
  • Syntax highlighting
  • Refinement
  • Auto
  • Infer type of goal contents
  • Jumping between goals
  • Expression normalization and type inference
  • Give contents to goals

*: (more like is sort of working, but everything is still experimental...)

In Progress

  • Code quality improvements

Planned

  • Inline case split
  • Go to definition

Note: Unicode input is not yet implemented, use digraphs! Some examples for special characters that you can enter by default:

  • ∀ = ^KFA ("For All")
  • ∃ = ^KTE ("There Exists")
  • → = ^K->
  • λ = ^Kl*
  • ≡ = ^K=3
  • ¬ = ^KNO

Thanks to

  • u/algebrartist for help with the development on reddit and testing
  • banacorn for agda-mode-vscode and the description of the communication protocol
  • jliptrap for doing initial testing and reporting issues