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

Jump to bottom

Auto complete should add meta tags #6

Open

derekyin opened this issue Nov 26, 2018 · 1 comment

Labels

Collaborator

derekyin commented Nov 26, 2018

Suggestions in auto complete should display meta tags that identifies what set of rules the suggestion came from

derekyin added the enhancement label

Owner

ShazzAmin commented Nov 26, 2018

To add to that, maybe we can also push to the top of the suggestions the rule names that correspond to the current "#check" the user is in.

e.g. if the user is working on an ND proof (and they're within a "#check ND"), we prioritize ND rules (maybe even filter to only show them)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment