ctrl-space in VS Code

Stream: general

[Kevin Buzzard]

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]

I find this really annoying.

[Chris Hughes]

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]

Would you mind opening an issue at leanprover-community/lean? This is something that would have to be changed in C++.