agda/cornelis

Issues

• Support re-using buffers

  #164 opened a month ago by 4e554c4c
  0

• dont set `ft=agda` for literate agda

  #157 opened a month ago by 4e554c4c
  0

• Type Inference does not work

  #159 opened 3 months ago by ANinjaRabbit
  1

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

  #161 opened 2 months ago by jakio6
  0

• Add cornelis plugin definition for NixVim

  #160 opened 3 months ago by flgrubm
  0

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

  #117 opened 2 years ago by 4e554c4c
  8

• it says file is not executable

  #158 opened 4 months ago by ARBS-hmm
  1

• Goto Definition is off by one

  #154 opened 7 months ago by m0rphism
  3

• Spin out the `agda-input` part into it's own plugin?

  #142 opened 8 months ago by silky
  6

• Inputting the "agda input prefix" as a literal

  #148 opened 10 months ago by googleson78
  5

• Highlighting group CornelisType only affects InfoWindow

  #153 opened 8 months ago by milaurila
  4

• Hackage distribution is missing test files

  #150 opened 9 months ago by phijor
  1

• Loading of read-only modules fails

  #116 opened 9 months ago by phijor
  0

• Publishing to Hackage

  #147 opened 10 months ago by phijor
  1

• Vimscript: is this a design choice?

  #144 opened a year ago by lane-core
  3

• `star` is bound twice

  #139 opened a year ago by silky
  1

• `CornelisRefine` on unknown seems to print Aeson JSON instead of ... something?

  #141 opened a year ago by silky
  0

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

  #138 opened a year ago by silky
  1

• lazy.nvim build fails `ar: conftest.a: No such file`

  #135 opened a year ago by gwimm
  1

• Can't find interaction point 0

  #133 opened a year ago by JonathanLorimer
  3

• `CornelisUnsolvedMeta` highlight does not appear some of the time

  #125 opened a year ago by 4e554c4c
  5

• Addition of Latex input bindings causing parse error

  #129 opened a year ago by epeery
  1

• Add more bindings inherited from Tex Input Method?

  #128 opened a year ago by favonia
  6

• How to check type of term under cursor

  #127 opened a year ago by langfield
  6

• `:CornelisSolve` does not do anything

  #124 opened a year ago by 4e554c4c
  1

• Splitting inside lambda using where-block causes unhandled exception

  #121 opened 2 years ago by mbrea-c
  1

• Sometimes makes extra scratch buffers

  #119 opened 2 years ago by llllvvuu
  0

• Do syntax highlighting for cubical terms in infowin

  #68 opened 2 years ago by isovector
  2

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

  #113 opened 2 years ago by isovector
  2

• Provide snippets for unicode selection

  #108 opened 2 years ago by 4e554c4c
  5

• Correctly pass ranges to Agda when operating over IPs

  #97 opened 2 years ago by isovector
  3

• Add haddock for everything

  #73 opened 2 years ago by isovector
  0

• Support -l in agsy

  #93 opened 2 years ago by isovector
  0

• Utils for debugging

  #99 opened 2 years ago by Lysxia
  1

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

  #109 opened 2 years ago by isovector
  0

• Cornelis not loading properly for .lagda.md files

  #61 opened 2 years ago by aricursion
  4

• `Unknown function: nvimhs#start`

  #100 opened 2 years ago by Zelatrix
  6

• Unicode input regression

  #96 opened 2 years ago by Lysxia
  2

• Case split asks for what to split even if the goal is full

  #92 opened 2 years ago by isovector
  1

• QuestionToMeta doesn't work for ?)

  #91 opened 2 years ago by isovector
  1

• Minor highlighting issue

  #88 opened 2 years ago by Lysxia
  2

• Tab completion for simplification modes

  #57 opened 2 years ago by isovector
  1

• Invisible goals are sometimes not highlighted

  #81 opened 2 years ago by Lysxia
  7

• Typo in arrow binding?

  #75 opened 3 years ago by chezbgone
  1

• Questionmarks are replaced by `{! !}` in non-hole positions

  #71 opened 3 years ago by phijor
  5

• Support for cubical path types

  #67 opened 3 years ago by NickHu
  4

• Make it possible to open the information window on the right instead of at the top

  #60 opened 3 years ago by JakobBruenker
  3

• Restrict height of the view with the goals

  #63 opened 3 years ago by Eloitor
  1

• ghc version

  #62 opened 3 years ago by Eloitor
  2

• Cmd_give after refinement / etc

  #58 opened 3 years ago by isovector
  0