a code suggestion bug

Stream: general

[fonqL]

lean version: 4.9.0-rc1
mwe:

def aaaaa := 1

#eval ([1,2,3].map λ c => a).length

LSP only suggests symbols in the namespace of List.

actual behavior

[Marc Huisinga]

I can reproduce this. Could you create a GitHub issue for it?

[fonqL]

Yes.
issues#4455

[Marc Huisinga]

Thanks!

[fonqL]

wait, a little embarrassed, what repo should I report to, lean4 or vscode-lean4 repo? :sweat_smile:

[Marc Huisinga]

The lean4 repository is correct here :-)

The completions are computed by the language server, which lives in the lean4 repository. vscode-lean4 is (for the most part) only the UI.