npm

cornelis

Neovim plugin providing interactive Agda proof assistance

brewmacoslinux
Try with needOr install directly
Source

About

Neovim support for Agda

Commands

cornelis

Examples

Start Neovim with Cornelis plugin for Agda development$ nvim myproof.agda
Load and typecheck an Agda file with Cornelis support$ nvim +':Cornelis' mytheorem.agda
Use Cornelis goal and refine commands in Agda buffer$ nvim +':CornelisGoals' proof.agda