tab completion

Stream: general

[Jeremy Avigad]

Here is a question that just came up in the lftcm session. Consider the following proof:

import data.real.basic algebra.big_operators data.fintype.basic

variables (n : Type) [fintype n] (f : n → ℝ)

example : finset.univ.sum f ≤ finset.univ.sum (λ i, f i + 1) :=
begin
  apply finset.sum_le_sum,
  intros, linarith
end

At the apply, it would be helpful if we could start typing sum_le and have tab completion help. But in VS Code, with sum_le, tab completion returns nothing, and even finset.sum_le_sum doesn't find it. But then sum_le_ finds the right fact.

Has there been a discussion on Zulip before about tab completion's mysterious ways?

[Yakov Pechersky]

In my experience, tab completion only provides things that are in its "cache", and ctrl-space has to be relied on to access more completion options.

[Yakov Pechersky]

It'd be nice if the ctrl-space options defaulted to the first type-relevant item. Maybe they already do.

[Bryan Gin-ge Chen]

I think @Kenny Lau made a few threads about the suggestions in the ctrl+space menu. Note that these are all provided to the VS Code extension by the Lean server, so it might be useful to open an issue on the community Lean repo with some examples.

[Jeremy Avigad]

Indeed, ctrl+space helps. That's good to know.