You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository has been archived by the owner on Feb 26, 2021. It is now read-only.
Sorry in advance for opening this issue here, feel free to close it if inappropriate.
It would be very nice if we could teach autocomplete-plus Agda's notion of what an identifier is. If we have some definition long-identifier-*, then at the moment it only suggests long as an identifier.
It’s interesting to note that there is a simple (i.e. incomplete) workaround for this problem.
In the autocomplete-plus package settings, you can set the “Extra Word Characters” setting to “-”, and it will start to recognize long-identifier-foo as a single word.
Sign up for freeto subscribe to this conversation on GitHub.
Already have an account?
Sign in.
Sorry in advance for opening this issue here, feel free to close it if inappropriate.
It would be very nice if we could teach autocomplete-plus Agda's notion of what an identifier is. If we have some definition
long-identifier-*
, then at the moment it only suggestslong
as an identifier.Has anyone started work on an autocomplete-plus provider for Agda?
I have no experience but would be willing to work on this if others are interested and willing to help out if I get stuck.
The text was updated successfully, but these errors were encountered: