Zulip Chat Archive

Stream: general

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: Dec 20 2023 at 11:08 UTC