Issues

• [Feat] vim.g.cornelis_agda_binary

  agda/cornelis#203 · Filter by author foxyseta opened on Oct 4, 2026

• Unicode issue in Windows

  agda/cornelis#202 · Filter by author fabrizio-m opened on Oct 1, 2026

• Module doesn't build: Couldn't match expected type ‘Window’ with actual type ‘Object’

  agda/cornelis#197 · Filter by author AxelFl opened on Jun 2, 2026
  5

• Support Cmd_show_module_contents_toplevel

  agda/cornelis#195 · Filter by author 4e554c4c opened on Mar 25, 2026

• Auto : last hole does not get filled

  agda/cornelis#193 · Filter by author leo-leesco opened on Jan 28, 2026

• Migrate away from stack

  help wanted
  Feature

  agda/cornelis#191 · Filter by author 4e554c4c opened on Jan 26, 2026

• :CornelisGive no longer working on Agda head

  agda/cornelis#186 · Filter by author 4e554c4c opened on Dec 8, 2025

• [BUG] CornelisGoToDefinition for datatypes

  agda/cornelis#185 · Filter by author foxyseta opened on Nov 4, 2025

• Make Case Doesn't expand variables into dot patterns

  agda/cornelis#180 · Filter by author eldritch-cookie opened on Oct 5, 2025

• Missing top command CornelisShowConstraints (Emacs C-c C-=)

  enhancementhelp wanted
  agda/cornelis#176 · Filter by author andreasabel opened on Jul 16, 2025
  4

• Holes (goals) are not numbered

  enhancementhelp wanted
  agda/cornelis#172 · Filter by author yzhanglbto opened on Mar 30, 2025
  2

• Support re-using buffers

  Feature

  agda/cornelis#164 · Filter by author 4e554c4c opened on Jan 15, 2025

• get "No goal at cursor" when there is one

  Bug

  agda/cornelis#161 · Filter by author jakio6 opened on Dec 17, 2024

• Type Inference does not work

  Bug

  agda/cornelis#159 · Filter by author ANinjaRabbit opened on Nov 24, 2024
  2

• Goto Definition is off by one

  agda/cornelis#154 · Filter by author m0rphism opened on Jul 15, 2024
  3

• Highlighting group CornelisType only affects InfoWindow

  agda/cornelis#153 · Filter by author milaurila opened on Jun 14, 2024
  5

• Inputting the "agda input prefix" as a literal

  agda/cornelis#148 · Filter by author googleson78 opened on May 7, 2024
  5

• Vimscript: is this a design choice?

  enhancementhelp wanted
  Feature

  agda/cornelis#144 · Filter by author biocini opened on Mar 22, 2024
  9

• Multi-line comment quirk - it inserts single-line comment prefixes

  agda/cornelis#138 · Filter by author silky opened on Feb 20, 2024
  1

• Splitting inside lambda using where-block causes unhandled exception

  agda/cornelis#121 · Filter by author mbrea-c opened on Jul 29, 2023
  1

• Syntax is lost after go-to-def (or editing a file)

  bughelp wanted
  Bug

  agda/cornelis#117 · Filter by author 4e554c4c opened on Apr 5, 2023
  8

• Don't jump to top of file when refining an hole with a type error

  bugwontfix
  Bug

  agda/cornelis#113 · Filter by author isovector opened on Feb 9, 2023
  3

• Agda identifiers don't correctly get tackled by vim movements

  blocked upstream
  agda/cornelis#109 · Filter by author isovector opened on Jan 26, 2023

• Correctly pass ranges to Agda when operating over IPs

  question
  agda/cornelis#97 · Filter by author isovector opened on Nov 22, 2022
  3

• Support -l in agsy

  enhancement
  agda/cornelis#93 · Filter by author isovector opened on Nov 4, 2022