Zulip Chat Archive

Stream: general

Topic: suggestions missing

Kenny Lau (Jul 09 2020 at 10:58):

why doesn't VSCode suggest foo.bar?

Kevin Buzzard (Jul 09 2020 at 11:02):

import tactic

class foo (α : Type) : Type :=
(bar : ℕ)

#check foo.bar

example : Π (α : Type) [c : foo α], ℕ := by suggest

/-
Try this: exact foo.bar
Try this: exact foo.sizeof
-/

Kevin Buzzard (Jul 09 2020 at 11:02):

Note that I changed Type* to Type

Kevin Buzzard (Jul 09 2020 at 11:03):

I put the universe variable back and I still get the suggestion

Kenny Lau (Jul 09 2020 at 11:04):

oh btw I'm talking about the Ctrl+Space auto-completion

Kevin Buzzard (Jul 09 2020 at 11:04):

oh right. Yes, I don't get the auto-completion either

Kevin Buzzard (Jul 09 2020 at 11:05):

#check foo.m suggests mk, but #check foo.b doesn't suggest bar

Kenny Lau (Jul 14 2020 at 06:45):

@Gabriel Ebner

Kenny Lau (Jul 21 2020 at 11:18):

Quī appellāmus?

Johan Commelin (Jul 21 2020 at 11:20):

Mi no save long toktok bilong yu

Kenny Lau (Jul 21 2020 at 11:22):

Who shall we summon?

Kenny Lau (Jul 21 2020 at 11:22):

I've just created an issue: https://github.com/leanprover/vscode-lean/issues/212

Bryan Gin-ge Chen (Jul 21 2020 at 11:24):

This is really a Lean server issue.

Last updated: Dec 20 2023 at 11:08 UTC