Mathlib symbols not showing in VSCode for suggestions

Stream: new members

[Anand Jain]

image.png
Just a second ago it seemed like I could type a few characters and hit Ctrl Enter and it would find me symbols in mathlib that matched. For some reason these symbols arent showing up. What am I doing wrong? Thanks

[Anand Jain]

I tried restarting the LSP but that didn't help

[Kevin Buzzard]

I don't know much about autocompletion but I think it might depend on the context. For example try #check bij (so now lean is expecting a term, not a command) and see if you get different answers.

[Anand Jain]

image.png
Thank you Kevin!

[Anand Jain]

image.png
Is it expected that loading symbols from mathlib takes more than 2 minutes? I've been waiting for a while for symbols in Mathlib.Data to load but it doesn't seem like it will

[Marc Huisinga]

Anand Jain said:

image.png
Is it expected that loading symbols from mathlib takes more than 2 minutes? I've been waiting for a while for symbols in Mathlib.Data to load but it doesn't seem like it will

Does it work if you press Escape and Ctrl+Space again to retrigger the completion?

[Marc Huisinga]

There are some known issues with the import completion mechanism that should be fixed in the next release candidate (lean4#7178)

[Anand Jain]

Weird now it seems to be working, it takes maybe 10 seconds to load symbols now.
Since I have you what is the difference between FinSet and Finset. I cannot seem to get docstring
image.png. I tried searching for FinSet on the mathlib docs but it seems like there is only Finite.Set which I cannot seem to find

[Anand Jain]

All I'm trying to do is get the set of bijections from F->F. (trying to prove that this set forms a group under composition) but I can't seem to figure out how to set everything up properly

[Kevin Buzzard]

FinSet isn't a thing, and if you write it in a project which has got the autoImplicit footgun set to true (the default setting) then Lean just creates a random new type called FinSet in order to make your life easier / completely confuse you depending on your level of comprehension of the system.

[Marc Huisinga]

On v4.18.0-rc1, the auto-implicit is now displayed explicitly as such:
Auto-implicit inlay hint

[Anand Jain]

I think I got it variable (S : { f : Finset α → Finset α // Function.Bijective f})

[Anand Jain]

Actually I think this might be wrong, because I'm trying to say the collection of bijections from a finite set to itself, which I don't think Finset \alpha to Finset \alpha means

[Kevin Buzzard]

Finset \alpha is the type of all finite subsets of \alpha.