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

More intelligent binding suggestions #40

Open
cb372 opened this issue Nov 16, 2020 · 0 comments
Open

More intelligent binding suggestions #40

cb372 opened this issue Nov 16, 2020 · 0 comments
Labels

Comments

@cb372
Copy link
Owner

cb372 commented Nov 16, 2020

In the Relevant bindings include... section, currently we list all the bindings we can find. It would be nice to use the type of the hole to prioritise these bindings in some way, and maybe filter out any that are clearly irrelevant.

There's a wide spectrum of how clever we want to be with this. We need to be careful not to accidentally write our own typechecker or go too far down the road of Idris-style proof search or Curry-Howard correspondence. I'd like to see how far we could get with just some simple heuristics first.

@cb372 cb372 added the LSUG label Nov 16, 2020
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

1 participant