cornelis

{
  "aliases": [],
  "alternatives": [],
  "build_dependencies": [
    "cabal-install",
    "ghc",
    "hpack"
  ],
  "categories": [],
  "caveats": null,
  "conflicts_with": [],
  "dependencies": [
    "gmp"
  ],
  "deprecated": 0,
  "deprecation_reason": null,
  "desc": "Neovim support for Agda",
  "disable_reason": null,
  "disabled": 0,
  "enrichment_fetched_at": "2026-06-20T23:36:36+00:00",
  "first_seen": "2026-06-20T23:34:18+00:00",
  "full_name": "cornelis",
  "github_default_branch": "master",
  "github_last_commit_at": "2026-06-02T12:16:50Z",
  "github_readme_excerpt": "# cornelis\n\n![Cornelis in Action](https://raw.githubusercontent.com/isovector/cornelis/master/cast.gif)\n\n\n## Dedication\n\n\u003e I\u0027ll ask to stand up \\\n\u003e With a show about a rooster, \\\n\u003e Which was old and worn out, \\\n\u003e Impotent and weathered. \\\n\u003e The chickens complained and whined \\\n\u003e Because he did not satisfy them.\n\u003e\n\u003e -- [Cornelis Vreeswijk](https://www.youtube.com/watch?v=oKUscEWPVAM)\n\n## \u26a0\ufe0f Maintenance Status \u26a0\ufe0f\n\nThis repository is currently **unmaintained**.\n\nPlease reach out to the [agda community](https://wiki.portal.chalmers.se/agda/Main/Community)\nif you are interested in maintaining Cornelis.\n\n## Overview\n\n`cornelis` is [agda-mode], but for neovim. It\u0027s written in Haskell, which means\nit\u0027s maintainable and significantly less likely to bit-rot like any\nvimscript/lua implementations.\n\n[agda-mode]: https://agda.readthedocs.io/en/latest/tools/emacs-mode.html\n\n## Features\n\nIt supports highlighting, goal listing, type-context, refinement, auto, solving,\ncase splitting, go-to definition, normalization, and helper functions. These are\nexposed via vim commands.  Most commands have an equivalent in [agda-mode].\n\n### Global commands\n\n| Vim command | Description | Equivalent agda-mode keybinding |\n| :--- | :--- | :--- |\n| `:CornelisLoad`             | Load and type-check buffer | \u003ckbd\u003eC-c\u003c/kbd\u003e\u003ckbd\u003eC-l\u003c/kbd\u003e |\n| `:CornelisGoals`            | Show all goals        | \u003ckbd\u003eC-c\u003c/kbd\u003e\u003ckbd\u003eC-?\u003c/kbd\u003e |\n| `:CornelisRestart`          | Kill and restart the `agda` process | \u003ckbd\u003eC-c\u003c/kbd\u003e\u003ckbd\u003eC-x\u003c/kbd\u003e\u003ckbd\u003eC-r\u003c/kbd\u003e |\n| `:CornelisAbort`            | Abort running command | \u003ckbd\u003eC-c\u003c/kbd\u003e\u003ckbd\u003eC-x\u003c/kbd\u003e\u003ckbd\u003eC-a\u003c/kbd\u003e |\n| `:CornelisSolve \u003cRW\u003e`       | Solve constraints     | \u003ckbd\u003eC-c\u003c/kbd\u003e\u003ckbd\u003eC-s\u003c/kbd\u003e |\n| `:CornelisGoToDefinition`   | Jump to definition of name at cursor | \u003ckbd\u003eM-.\u003c/kbd\u003e or middle mouse button |\n| `:CornelisPrevGoal`         | Jump to previous goal | \u003ckbd\u003eC-c\u003c/kbd\u003e\u003ckbd\u003eC-b\u003c/kbd\u003e |\n| `:CornelisNextGoal`         | Jump to next goal     | \u003ckbd\u003eC-c\u003c/kbd\u003e\u003ckbd\u003eC-f\u003c/kbd\u003e |\n",
  "github_repo": "agda/cornelis",
  "github_stars": 184,
  "github_topics": [
    "agda",
    "neovim",
    "nvim-hs",
    "vim-textobj-user",
    "vim-which-key"
  ],
  "homepage": "https://github.com/agda/cornelis",
  "homepage_og_description": null,
  "homepage_og_image": null,
  "homepage_title": null,
  "installs_30d": 5,
  "installs_365d": 110,
  "installs_90d": 32,
  "keg_only": 0,
  "keg_only_reason": null,
  "last_seen": "2026-06-20T23:34:18+00:00",
  "license": "BSD-3-Clause",
  "llm_generated_at": null,
  "llm_model": null,
  "name": "cornelis",
  "oldnames": [],
  "one_liner": null,
  "optional_dependencies": [],
  "rank_30d": 10445,
  "rank_365d": 8924,
  "rank_90d": 8497,
  "raw_hash": "507ebbcdd4aac4b2",
  "recommended_dependencies": [],
  "revision": 0,
  "ruby_source_path": "Formula/c/cornelis.rb",
  "tap": "homebrew/core",
  "test_dependencies": [],
  "uses_from_macos": [
    "libffi"
  ],
  "version_head": "HEAD",
  "version_stable": "2.8.0",
  "versioned_formulae": [],
  "why_use_this": null
}