Zulip Chat Archive

Stream: general

Topic: tab completion

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) :=
  apply finset.sum_le_sum,
  intros, linarith

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 (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.

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.

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.

Jeremy Avigad (Jul 17 2020 at 16:01):

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

Last updated: Dec 20 2023 at 11:08 UTC