cornelis for Mac

Dedication I'll ask to stand up With a show about a rooster, Which was old and worn out, Impotent and weathered. The chickens complained and whined Because he did not satisfy them. -- Cornelis Vreeswijk

⚠️ Maintenance Status ⚠️

This repository is currently in the process of switching maintainers. There will likely be a slow response time for PRs and feature requests during this ramp-up period.

If you are having issues building or running cornelis, please check COMPATIBILITY.md first before opening an issue!

Overview

cornelis is [agda-mode], but for neovim. It's written in Haskell, which means it's maintainable and significantly less likely to bit-rot like any vimscript/lua implementations.

Features

It supports highlighting, goal listing, type-context, refinement, auto, solving, case splitting, go-to definition, normalization, and helper functions. These are exposed via vim commands. Most commands have an equivalent in [agda-mode].

Global commands

Commands in context of a goal

These commands can be used in context of a hole:

Commands with an ` argument take an optional normalization mode argument, one of AsIs, Instantiated, HeadNormal, Simplified or Normalised. When omitted, defaults to Normalised. This default may be specified in vimrc as g:cornelis_rewrite_mode.

Commands with a argument take an optional compute mode argument:

If Agda is stuck executing a command (e.g. if normalization takes too long), abort the command with :CornelisAbort.

If you need to restart the plugin (eg if Agda is stuck in a loop), you can restart everything via :CornelisRestart.

Agda Input

There is reasonably good support for agda-input via your in insert mode. See

for available bindings.

If you'd like to use a prefix other than your , add the following to your .vimrc:

Interactive Unicode Selection

If you'd like an interactive prompt for choosing unicode characters, additionally install vim-which-key:

and map a call to cornelis#prompt_input() in insert mode:

Disabling Default Bindings

If you don't want any of the default bindings, add the following to your .vimrc:

Adding Bindings

Custom bindings can be added by calling the cornelis#bind_input function in .vimrc. For example:

will add nat as an input remapping for ℕ.

The inverse of cornelis#bind_input("foo", "...") is cornelis#unbind_input("foo"). Note that this cannot and will not attempt to undo any custom agda-input management, such as through g:cornelis_bind_input_hook (see below).

Custom Hooks

If you'd prefer to manage agda-input entirely on your own (perhaps in a snippet system), you can set the following:

You can invoke cornelis#standard_bind_input with the same arguments if you'd like to run your hook in addition to the standard one.

Text Objects

Use the iz/az text objects to operate on text between ⟨ and ⟩. Somewhat surprisingly for i/a text objects, iz targets the _spaces_ between these brackets, and az targets the spaces. Neither textobj targets the brackets themselves.