Skip to content
This repository has been archived by the owner on Feb 26, 2021. It is now read-only.

Issues: banacorn/agda-mode

24 Open 88 Closed
24 Open 88 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

All undo commands are doubled
#132 opened Dec 23, 2020 by elidupree
support for literate Markdown Agda?
#130 opened Aug 20, 2020 by lclem
QuickLaTeX backend howto? willdo
#127 opened May 28, 2020 by pnlph
5
Hole not expanding when placed before a closing parenthesis
#126 opened May 20, 2020 by banacorn
Go to definition for mixfix operators without underscore fails bug
#125 opened May 16, 2020 by pnlph
1
Scope info does not provide links for the openings enhancement
#122 opened Mar 22, 2020 by pnlph
4
Interacting within agda code in Atom
#121 opened Mar 21, 2020 by pnlph
3
Update README with Emacs/Atom commands
#119 opened Jan 3, 2020 by pnlph
2
Unicode input doesn't work bug
#113 opened Sep 11, 2019 by bgavran
11
Non-termination of Agda file loading
#106 opened Jul 10, 2019 by vieillevigne
3
The errors are incorrectly located
#99 opened May 20, 2019 by mrakgr
7
integration with linter enhancement
#87 opened Mar 5, 2019 by ghost
1
header text overflows incorrectly bug Reimplement in Reasonml To be reimplemented and fixed in Reasonml
#86 opened Mar 5, 2019 by ghost
3
use user editor font information enhancement Reimplement in Reasonml To be reimplemented and fixed in Reasonml
#85 opened Mar 5, 2019 by ghost
4
problems with pane‐positioning Reimplement in Reasonml To be reimplemented and fixed in Reasonml
#83 opened Mar 5, 2019 by ghost
1
Key binding changes should be for agda files only
#78 opened Jan 17, 2019 by freeman42x
6
autocomplete-plus provider for Agda enhancement help wanted
#73 opened Oct 16, 2018 by buggymcbugfix
3
Missing commands enhancement willdo
#67 opened Aug 16, 2018 by gallais
1
.lagda.md support enhancement help wanted
#65 opened Aug 2, 2018 by jonaprieto
2
floating of goal numbers bug
#64 opened Jul 31, 2018 by jonaprieto
1
Write tests essential help wanted
#28 opened Jan 12, 2016 by banacorn
6 of 11 tasks
2
Coping with ctrl+c on windows bug help wanted
#19 opened Jul 7, 2015 by cnd
7
Input Symbol only works from Cmd+Shift+P help wanted
#10 opened May 7, 2015 by TheoWinterhalter
26
Syntax Highlighting enhancement help wanted
#5 opened Feb 8, 2015 by banacorn
6
ProTip! Mix and match filters to narrow down what you’re looking for.