Topic: ctrl-space in VS Code
Kevin Buzzard (Nov 19 2019 at 18:57):
Just learnt this:
import data.list.basic #check list.length_zero -- ctrl-space suggests "list.length_eq_zero" open list #check list.length_zero -- ctrl-space suggests nothing
I have seen ctrl-space not giving me as many results as I was hoping for, but I'd not realised that this was a possible issue.
Chris Hughes (Nov 19 2019 at 19:07):
I find this really annoying.
Chris Hughes (Nov 19 2019 at 19:08):
Often I open
nat, but I still want to make sure I get a
nat lemma, and not the corresponding group version, but that is difficult with this behaviour.
Bryan Gin-ge Chen (Nov 19 2019 at 19:42):
Would you mind opening an issue at leanprover-community/lean? This is something that would have to be changed in C++.
Last updated: May 06 2021 at 21:09 UTC