cornelis
cornelis copied to clipboard
isovector
agda-mode for neovim
I'm starting forget how this code works; better write it down before it all fades away :)
Right now Agda just dumps out some strings to show. It's fine but they're structured and easy enough to give some coloring to
Hi! I"m having an issue specifically with `.lagda.md` files. Whenever I try to load them, my neovim just recognizes them as regular markdown files. Because of this, I can't seem...
Cmd_give lets agda update its internal state without requiring a subsequent reload. emacs asks for a refinement and then immediately gives it back. Cornelis should do the same. Can we...
Set a `CmdComplete` `CommandOption`, and then follow the docs: ``` The following example lists user names to a Finger command :com -complete=custom,ListUsers -nargs=1 Finger !finger :fun ListUsers(A,L,P) : return system("cut...
When agda is running slow, it's easy to get ahead of the highlighter, and the resulting big error messages are annoying.
Allegedly `line2byte` in vim does the line offsetting that we'd like.
It'd be nice to have a big testsuite here, just to really cement `cornelis` as the one true agda plugin for vim.
The one used for `TypeContext`, `Solve`, `Auto`, `Normalize`, `HelperFunc`. Use a global variable, configurable from vimrc.
If we have multiple values to split inside of a lambda split, subsequent splitting will replace old cases