Skip to content

Issues: agda/cornelis

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

20 Open 78 Closed
20 Open 78 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Type Inference does not work
#159 opened Nov 24, 2024 by ANinjaRabbit
it says file is not executable
#158 opened Oct 24, 2024 by ARBS-hmm
1
dont set ft=agda for literate agda
#157 opened Oct 10, 2024 by 4e554c4c
Goto Definition is off by one
#154 opened Jul 15, 2024 by m0rphism
3
Highlighting group CornelisType only affects InfoWindow
#153 opened Jun 14, 2024 by milaurila
4
Inputting the "agda input prefix" as a literal
#148 opened May 7, 2024 by googleson78
5
Vimscript: is this a design choice?
#144 opened Mar 22, 2024 by lane-core
3
CornelisRefine on unknown seems to print Aeson JSON instead of ... something?
#141 opened Feb 20, 2024 by silky
Multi-line comment quirk - it inserts single-line comment prefixes
#138 opened Feb 20, 2024 by silky
1
Can't find interaction point 0
#133 opened Dec 13, 2023 by JonathanLorimer
3
Splitting inside lambda using where-block causes unhandled exception
#121 opened Jul 29, 2023 by mbrea-c
1
Syntax is lost after go-to-def (or editing a file)
#117 opened Apr 5, 2023 by 4e554c4c
8
Don't jump to top of file when refining an hole with a type error bug Something isn't working
#113 opened Feb 9, 2023 by isovector
2
Agda identifiers don't correctly get tackled by vim movements blocked upstream
#109 opened Jan 26, 2023 by isovector
Correctly pass ranges to Agda when operating over IPs question Further information is requested
#97 opened Nov 22, 2022 by isovector
2 of 3 tasks
3
Support -l in agsy enhancement New feature or request
#93 opened Nov 4, 2022 by isovector
Cmd_give after refinement / etc
#58 opened Jun 16, 2022 by isovector
Make the rewrite mode modifiable configuration
#41 opened Feb 17, 2022 by isovector
Investigate using line2byte for highlighting vim
#21 opened Feb 1, 2022 by isovector
2
Don't assume agda is on the path configuration
#12 opened Jan 29, 2022 by isovector
1
ProTip! Mix and match filters to narrow down what you’re looking for.