name completion

Stream: lean4

[Chris Birkbeck]

I'm very new to lean 4, so sorry if this is a stupid question. But does lean 4 have an auto-complete for names of basic lemmas like in lean 3? Fore example, in lean 3 I can start typing div_ and it will suggest lemmas with that in the name? I don't know if this is something that needs to be enabled somewhere.

[Henrik Böving]

Yes it does have auto completion but I don't think fuzzy one (?) i.e. it will give you identifiers that start with that name. It also triggers on . like Nat. ....

[Julian Berman]

See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/autocomplete.20woes

[Chris Birkbeck]

Oh I see thanks. I think it was just being much slower!