Zulip Chat Archive

Stream: general

Topic: tab completion


view this post on Zulip Jeremy Avigad (Jul 17 2020 at 13:21):

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?

view this post on Zulip Yakov Pechersky (Jul 17 2020 at 13:47):

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.

view this post on Zulip Yakov Pechersky (Jul 17 2020 at 13:47):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 17 2020 at 13:48):

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.

view this post on Zulip Jeremy Avigad (Jul 17 2020 at 16:01):

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


Last updated: May 14 2021 at 14:20 UTC