cornelis ☆

« Back to VersTracker

Description:
Neovim support for Agda

Type: Formula | Latest Version: 2.8.0@0 | Tracked Since: Dec 17, 2025

Links: Homepage | formulae.brew.sh

Category: Developer tools

Tags: agda neovim proof-assistant plugin verification

Install: brew install cornelis

About:
Cornelis is a Neovim plugin that provides interactive support for the Agda proof assistant. It integrates directly into the editor to offer features like goal manipulation, case splitting, and type checking. This tool streamlines the proof development workflow for Agda users within their preferred editor environment.

Key Features:

Interactive goal filling and exploration
Automatic case splitting and type-based search
Syntax highlighting and error diagnostics
Integration with Neovim's LSP ecosystem

Use Cases:

Developing formal proofs and verified software in Agda
Interactive theorem proving with editor feedback
Refactoring complex Agda codebases

Alternatives:

agda-mode – The standard Emacs mode for Agda; Cornelis provides a comparable experience for Neovim users.

License: BSD-3-Clause

Dependencies: gmp

Bottles available for: arm64_tahoe, arm64_sequoia, arm64_sonoma, arm64_ventura, sonoma, ventura, arm64_linux, x86_64_linux

Version History

Detected	Version	Rev	Change	Commit
Sep 14, 2025 2:17am		0	VERSION_BUMP	f8033330