Skip to content
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.

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

delete.type autocompletion skips over types #4190

Open
ceedubs opened this issue Jul 11, 2023 · 1 comment
Open

delete.type autocompletion skips over types #4190

ceedubs opened this issue Jul 11, 2023 · 1 comment
Labels

Comments

@ceedubs
Copy link
Contributor

ceedubs commented Jul 11, 2023

Add a type like unique type Foo = Foo Nat and then in ucm type delete.type Fo<TAB>. It completes to delete.type Foo. and if you hit enter it displays the curious message I don't know how to parse.

Instead it should autocomplete to delete.type Foo.

Separately that error message should probably be fixed.

@ceedubs ceedubs added the bug label Jul 11, 2023
@sixfourtwelve
Copy link
Contributor

sixfourtwelve commented Sep 8, 2023

Happy to take, seems the issues I like most are yours @ceedubs :)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants